¿La demostración formal (la matemática formalizada) es interesante para los matemáticos en activo? ¿Para los educadores?

Question

Formalizar las pruebas matemáticas para que puedan ser comprobadas y manipuladas por ordenador es una propuesta recurrente, sobre todo en el manifiesto QED (1994). El sitio web Número de diciembre de 2008 de Avisos de la AMS está enteramente dedicado al estado del arte de las pruebas formales; el sitio web de Cameron Freer, vdash.org, ofrece una visión general e informal.

Como matemáticos en activo, ¿cuál es su percepción de las pruebas formales y los asistentes de pruebas interactivos? ¿Están familiarizados con los sistemas actuales? ¿Deberían utilizarse en la enseñanza de las matemáticas?

¿Cuáles son los obstáculos para que la demostración formal se convierta en una herramienta de uso generalizado, además del esfuerzo necesario para construir una biblioteca útil de conocimientos matemáticos actuales?

Answer 1

Creo que esto se está utilizando para verificar los resultados, en particular la conjetura de Kepler, por el proyecto Flyspeck. Así que ahora es una forma de intentar demostrar teoremas y, por tanto, es de interés para los matemáticos en activo.

Answer 2

No estoy seguro de que la pregunta sea realmente una pregunta de MO, pero picaré; los tres mayores obstáculos son:

• una base de datos de teoremas (es la más fácil)

• un algoritmo razonable que pueda salvar pasos triviales (se está intentando construir uno desde hace años)

• un lenguaje razonable (lo más cercano que tiene es Mizar, y está muy lejos de la forma en que escribimos las matemáticas)

En el estado actual de las ferias, no creo que sean útiles ni siquiera como verificadores de pruebas, y mucho menos como asistentes de pruebas (no me refiero a los CAS, sino a los verificadores de autoprueba).

Answer 3

Carlos Simpson, en los años noventa escribió "Descente pour les n-champs" junto con Andre Hirschowitz. Parece que se adelantaron a su tiempo: No se pudo encontrar a nadie que revisara su trabajo. Así que para saber si es correcto o no, Simpson empezó a desarrollar un programa de comprobación automática de teoremas para afirmaciones teóricas de categorías. Más tarde resultó que había una pequeña inexactitud (usaban cubiertas donde necesitaban hipercubiertas), pero no sé si se encontró con la ayuda del programa... En cualquier caso, muestra claramente cómo puede ser útil.