Formal Proof - Historial de revisiones

Jalonso en 09:28 11 dic 2008

2008-12-11T09:28:49Z

Jalonso en 09:27 11 dic 2008

2008-12-11T09:27:44Z

Jalonso en 09:26 11 dic 2008

2008-12-11T09:26:52Z

Jalonso: New page: T. Hales [http://www.ams.org/notices/200811/tx081101370p.pdf Formal Proof].

2008-12-11T08:57:13Z

New page: T. Hales [http://www.ams.org/notices/200811/tx081101370p.pdf Formal Proof].

Página nueva

T. Hales [http://www.ams.org/notices/200811/tx081101370p.pdf Formal Proof].

← Revisión anterior		Revisión del 09:28 11 dic 2008
Línea 23:		Línea 23:

	El artículo es de lectura agradable y resulta muy estimulante.		El artículo es de lectura agradable y resulta muy estimulante.
		+
		+	[[User:Jalonso\|José A. Alonso]] 11 Diciembre 2008
		+	[[Category:Lecturas]]

@@ Línea 20: / Línea 20: @@
 La sección 7 la dedica al proyecto QED. Inscribe el proyecto Flyspec dentro de los objetivos del manifiesto QED. Termina proponiendo el reto de la '''secuenciación del genoma matemático''':
-: ''To undertake the formalization of jus 100, 000 pages of core mathematics would be one of the most ambitious collaborative projects eve
+: ''To undertake the formalization of jus 100, 000 pages of core mathematics would be one of the most ambitious collaborative projects eve undertaken in pure mathematics, the sequencing of a mathematical genome. One might imagine a massive wiki collaboration that settles the text o the most signiﬁcant theorems in contemporary mathematics from Poincaré to Sato-Tate.''
 El artículo es de lectura agradable y resulta muy estimulante.

← Revisión anterior		Revisión del 09:26 11 dic 2008
Línea 1:		Línea 1:
−	T. Hales [http://www.ams.org/notices/200811/tx081101370p.pdf Formal Proof].	+	T. Hales [http://www.ams.org/notices/200811/tx081101370p.pdf Formal Proof]. Notices of the AMS, Vol. 55, N. 11 (2008) p.1370-1380.
		+	----
		+	Este trabajo es el primer artículo del [http://www.ams.org/notices/200811/ número de Diciembre de 2008 de las ''Notices of the AMS''] dedicado a las demostraciones formales.
		+
		+	El artículo comienza comentando los errores de programación (estima que se cometen 1.5 errores por línea cuando escribe código).
		+
		+	En la sección 1 comenta la certidumbre en matemáticas y sus problemas: supuestos implícitos (p.e. en la geometría griega) y demostraciones muy complejas (p.e. la de Almgren que ocupa 1.728 páginas). Así como el papel de los ordenadores en su certificación.
		+
		+	En la sección 2 trata de las demostraciones formales frente a las tradicionales. Comenta la dificultad de pasar de las segundas a la primera y recoge una tabla con algunas de las principales demostraciones formalizadas.
		+
		+	La sección 3 la dedica a comentar un sistema de razonamiento: el HOL Light. La elección debe de ser porque es en el que él trabaja. Contiene una detallada descripción de la lógica del sistema.
		+
		+	La sección 4 trata de sistemas de demostración automática. Comenta que no se han cumplido las profecías de la IA (1965)
		+	: ''a digital computer will discover and prove an important new mathematical theorem.''
		+	Sin embrago se han obtenido algunos éxitos como la demostración de la conjetura de Robbins, las demostraciones geométricas con el método de Wu y los procedimientos de decisión en algunas teorías.
		+
		+	La sección 5 trata del descubrimiento automático, desde el AM de Lenat hasta Graffiti.pc.
		+
		+	La sección 6 la dedica al proyecto Flyspec cuyo objetivo es la demostración formal de la conjetura de Kepler. Este proyecto es la razón por la que el autor se interesó por las demostraciones formalizadas. Cuenta la historia de la prueba de la conjetura y del proyecto.
		+
		+	La sección 7 la dedica al proyecto QED. Inscribe el proyecto Flyspec dentro de los objetivos del manifiesto QED. Termina proponiendo el reto de la '''secuenciación del genoma matemático''':
		+	: ''To undertake the formalization of jus 100, 000 pages of core mathematics would be one of the most ambitious collaborative projects eve
		+	undertaken in pure mathematics, the sequencing of a mathematical genome. One might imagine a massive wiki collaboration that settles the text o
		+	the most signiﬁcant theorems in contemporary mathematics from Poincaré to Sato-Tate.''
		+
		+	El artículo es de lectura agradable y resulta muy estimulante.