¿Ha pensado alguien en crear una wiki de pruebas formales con verificador?

Question

Las matemáticas han experimentado una evolución bastante agradable recientemente con la adopción de nuevas tecnologías, cosas como las revistas en línea, el arXiv, este sitio web, etc. Me imagino que debe haber muchos otros desarrollos que podrían ser muy útiles.

Lo que estoy pensando es en un sitio web en el que cualquiera pueda contribuir con demostraciones formales de teoremas. En particular, habría muchas pruebas del mismo teorema siempre que la prueba sea diferente - como una prueba constructiva del teorema del punto fijo de Brouwer, y una prueba no constructiva, etc.

La idea sería construir una gran red de pruebas formales, una sobre otra, de forma que se pudieran hacer búsquedas en este espacio de pruebas formales para averiguar cuáles son las pruebas más eficientes, en el sentido de cuántos caracteres ASCII se necesitarían para escribir la prueba utilizando la teoría de conjuntos de Zermelo-Frankel. Una esperanza sería tener una gran base de datos activa de pruebas formales verificadas. Otra sería tener una página web en la que se pudiera esperar descubrir si hay o no pruebas más sencillas de teoremas que se conocen y de las que no se tenía conocimiento.

Al ser una página web, habría ciertas eficiencias útiles: la página web podría "compilar" tu prueba y comprobar que es válida. Al ser un wiki, sería relativamente fácil para la gente contribuir y construir sobre una infraestructura existente. Y se podría utilizar libremente las pruebas preexistentes (siempre que se hayan verificado como válidas) en cualquier prueba posterior. Se podría comprobar fácilmente qué axiomas necesita una prueba, por ejemplo, hasta qué punto una prueba necesita el axioma de elección, etc.

¿Se ha hecho algún esfuerzo en este sentido? Es de esperar que esta herramienta funcione como el brazo editorial de una especie de Bourbaki moderno de la era de Internet.

Answer 1

Hay muchos sitios para pruebas formales, pero ninguna wiki que yo conozca.

Ejemplos típicos son:

archivo de pruebas formales en https://www.isa-afp.org/

Mizar http://mizar.org/

Las distribuciones de varios demostradores de teoremas interactivos contienen muchas pruebas: Isabelle, Hol, hol light, Coq, acl2, etc.

Como se dijo en otro post, no hay acuerdo sobre los fundamentos (fórmulas, axiomas y reglas de inferencia). Una división típica es entre sistemas clásicos (Hol et al.) y no clásicos (Coq et al.), pero las diferencias suelen ser mucho más sutiles que eso. Como resultado, todos estos sistemas son incapaces de reutilizar las pruebas de otros sistemas. Ocasionalmente, alguien escribe un traductor de un sistema a otro, pero el problema es que la traducción no suele producir una prueba legible en el sistema de destino; una prueba legible es necesaria para que la prueba traducida sea mantenible. Si te fijas en ZFC+ (tal vez algunos otros axiomas), entonces Mizar probablemente tiene la biblioteca más extensa.

Cada pocos años, alguien propone una gran base de datos de pruebas formales, pero estos proyectos mueren invariablemente por diversas razones relacionadas con las cuestiones anteriores. Un ejemplo es el proyecto QED:

http://en.wikipedia.org/wiki/QED_manifesto

Mi opinión personal es que construir pruebas formales, y mantenerlas, es actualmente demasiado difícil. Dicho esto, está claro que a largo plazo es una idea a la que le llegará su momento.

Answer 2

Esto existe; compruebe http://www.vdash.org/ y también esta charla de Cameron Freer: http://www.youtube.com/watch?v=ZDI7L4Ya9Ms .

Answer 3

Creo que los siguientes enlaces adicionales son relevantes:

http://homepages.inf.ed.ac.uk/da/mathwiki/

http://prover.cs.ru.nl/wiki.php

http://www.qedeq.org/ (más o menos)

Sin embargo, al igual que David Lehavi, soy escéptico sobre las ventajas de los wikis frente a la tecnología de los asistentes de pruebas habituales. Para mí, la barrera de entrada siempre ha sido aprender el lenguaje y las tácticas de un asistente de pruebas, no instalar el software o añadir algo a la biblioteca estándar (es decir, nunca he llegado tan lejos, pero si es un problema, entonces es un problema social).

Estoy de acuerdo con Tom Ridge en que ya llegará el momento de hacer una gran colección de matemáticas formales. Pero creo que deberíamos recopilar las definiciones, los enunciados de los teoremas y las pruebas por separado. Es decir, si un teorema ya es ampliamente conocido como verdadero, la demostración debería ser opcional, para que pueda ser completada más tarde. Una colección de definiciones formalizadas y hechos conocidos ya sería muy útil, y lo que es más importante, las personas que trabajan en diferentes pruebas pueden colaborar fácilmente, mientras que la formalización de definiciones y enunciados de teoremas requiere coordinación. Por supuesto, con los actuales asistentes de pruebas, es difícil estar seguro de que las definiciones y enunciados son correctos...

Answer 4

Como parte de la MathWiki de la Universidad de Radboud Nijmegen (Países Bajos), un wiki para Mizar y para Wiki de Coq-CoRN se construyeron. Sobre el teorema del punto fijo de Brouwer, por ejemplo, véase la entrada BROUWER en la wiki de Mizar.

Answer 5

Yo también he pensado en esto. Es algo para un futuro muy lejano.

Ya existe un lenguaje en el que la mayoría de los matemáticos están de acuerdo: El inglés. Un wiki de pruebas podría empezar con pruebas en texto plano, pero con una convención muy estricta, que permita una futura traducción a algún sistema de pruebas más fácil. Por ejemplo, véase la prueba original de D. Zeilberg de la conjetura de la matriz de signos alternos. Se presenta en inglés sencillo, pero el estilo es tal que cada parte es fácil de verificar.

En un futuro lejano, quizá sea posible verificar pruebas escritas en un estilo mucho más "suelto". De este modo, las pruebas en la wiki podrían acercarse gradualmente a ser verificables por ordenador, al mismo tiempo que los comprobadores de pruebas se vuelven cada vez más potentes. Eventualmente, habrá algún punto en el que las pruebas en este wiki puedan ser verificadas.