Razonamiento formalizado

Este es un megaproyecto. Según Thomas Hales "the formalization of just 100,000 pages of core mathematics" sería "the sequencing of a mathematical genome".

En este proyecto hay dos vías:

• De abajo arriba: Desarrollar el conocimiento básico común; es decir, el contenido en las licenciaturas e ingenierías. En esta vía, se elegiría algún curso y se procedería a la formalización del conocimiento matemático del mismo. Evidentemente, los cursos fundamentales son los de la Licenciatura en Matemáticas y los de la Ingeniería en Informática.
• De arriba abajo: Elegir un teorema importante (por ejemplo, alguno de la lista Formalizing 100 Theorems o de ...) y desarrollar el contenido matemático necesario para su verificación.

En ambos casos, lo importante no es la corrección del teorema final sino que aumente la comprensión del teorema por el autor de la prueba y sus futuros lectores. Por ello, es importante usar demostraciones estructuradas como las de Isabelle/Isar.

José A. Alonso 10:47, 19 November 2008 (CET)