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.
