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, list of projects in the area of formal mathematics o de Proofs from THE BOOK) 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.

Proyectos relacionados

1. IsarMathLib:

   A library of formalized mathematics for Isabelle/Isar proof assistant.

2. Tiddly Formal Math.

   Blog del proyecto IsarMathLib.

3. Formalized Mathematics.

   Revista de formalización en Mizar.

4. Journal of Formalized Reasoning.

   Nueva revista de razonamiento formalizado. El primer número es de 2008.

5. The Archive of Formal Proofs

   Biblioteca de formalizaciones en Isabelle.

6. Vdash:

   A formalized math wiki.

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