La mecánica de verificando pruebas por ordenador es prácticamente un problema resuelto. Tenemos un buen conocimiento de lo que es un paso de prueba válido y de cómo reconocer su validez por ordenador.
Lo que retrasa toda la empresa es que, aunque tenemos una buena teoría de la estructura de las pruebas, los ordenadores no entienden el inglés, por lo que las pruebas que queremos que comprueben deben traducirse al lenguaje formal con el que trabaja el comprobador de pruebas. El resultado suele parecerse más al código fuente de un programa que a la prosa matemática. Esta traducción aún no es del todo rutinaria, pero tampoco es un arte negro impenetrable.
Uno de los problemas es que existe una gran cantidad de conocimientos previos que, por lo general, los matemáticos que trabajan en la frontera de la investigación suponen ya conocidos. Antes de que los comprobadores de pruebas puedan empezar a trabajar con resultados contemporáneos, todo eso tiene que ser transcrito. Y la transcripción la tienen que hacer personas con conocimientos bastante sólidos de lógica y matemáticas, que podrían encontrar cosas más interesantes en las que emplear su tiempo.
Durante algún tiempo, ha sido posible obtener un doctorado cogiendo un trozo adecuado de matemáticas de licenciatura y formalizándolo en un sistema de pruebas informáticas. Pero la novedad va a desaparecer y, con el tiempo, dejará de impresionar a los comités de doctorado (puede que esto ya haya ocurrido, por lo que sé). Y luego, motivar a la gente para que haga el trabajo va a ser un verdadero problema. No es lo bastante conocido como para que los organismos de financiación pagar a cualquiera que haga el trabajo pesado, no por una cantidad suficiente de trabajo.
Creo que la esperanza general es que el desarrollo de bibliotecas de resultados acabe haciéndose mediante algún tipo de crowdsourcing, como el software de código abierto. Pero aún está por ver qué tipo de estructura de recompensa haría que eso funcionara.
1 votos
El mayor reto es desarrollar bibliotecas. Según [1], desarrollar una biblioteca para formalizar todas las matemáticas de pregrado llevará más de cien años-hombre. [1] A F. Wiedijk. Estimating the Cost of a Standard Library for a Mathematical Proof Checker, 2002. PDF .
6 votos
@J.D. En realidad, si esa estimación resultara ser correcta, no estaría tan mal y se vería empequeñecida por muchos productos de software de éxito que existen actualmente (pensemos en Word, Windows, etc.). En concreto, se ha estimado que el equipo de desarrollo de Windows 7, por ejemplo, estaba formado por más de 1000 desarrolladores .
1 votos
@3Esfera Cierto. Pero las empresas de software como Microsoft pueden ganar mucho dinero con grandes productos como Windows. No será el caso, por ejemplo, de una biblioteca Coq para demostrar teoremas de Sylow.