Problema de corrección de la prueba

Question

Estaba viendo esto hablar de Vladimir Voevodsky que se impartió en el Instituto de Estudios Avanzados en 2006.

En su charla, la primera diapositiva que muestra tiene escrito lo siguiente:

             We need to look at the foundations again because of the 

                         Proof correctness problem

Dos componentes:

$1.$ Hay un cúmulo de resultados cuyas pruebas la comunidad matemática no puede verificar completamente

$2.$ Cada vez hay más ejemplos de pruebas que han sido aceptadas y que luego se ha comprobado que son incorrectas

Este es un problema mucho más grave para las matemáticas que para cualquier ciencia, porque la principal fuerza de las matemáticas está en su capacidad de construir sobre múltiples capas de construcciones anteriores.

Esto es lo que dice mientras presenta la diapositiva:

"...... A medida que las matemáticas se hacen más complejas, se acumulan resultados cuya corrección es cada vez más incierta. No sabemos sobre ciertas cosas, si se han demostrado o no. ..... Todos los matemáticos han experimentado por ambos lados lo terrible que es hoy en día ser un árbitro. Tengo un artículo de unas 10 páginas que lleva unos 10 años en una revista porque el árbitro no puede pasar (no estoy seguro de haberle entendido bien). Yo mismo no he sido mucho mejor como árbitro. El problema es que las matemáticas son muy complejas y si uno quiere ser responsable de un artículo que arbitra, requiere un enorme esfuerzo. Realmente ralentiza las cosas. Tenemos que hacer algo al respecto. Desde mi punto de vista sólo hay una solución.... "

A continuación, habla de los fundamentos de las matemáticas, de la verificación automática de pruebas, etc. Mi pregunta se refiere únicamente a las afirmaciones $1.$ y $2.$ hecho en la diapositiva.

Q1. Estoy buscando ejemplos de tales resultados y pruebas. ¿Es este realmente un problema al que se enfrenta la comunidad matemática?

Q2. ¿Existe algún blog, artículo, ensayo, etc., que repase o enumere dichos resultados y pruebas, donde se discuta sobre estas cosas?

Answer 1

1) Esto se refiere a la cuestión de que las pruebas matemáticas se están convirtiendo en muy largo (algunos cientos de páginas, y aún así hay muchos pasos que se saltan porque el autor asume como trivial o como fácilmente reproducible. Eso en la práctica no siempre ocurre. Por ejemplo, se tardó años en confirmar la demostración del último teorema de Fermat. Sólo hay muy pocos expertos que puedan seguir la demostración con todo detalle y su tiempo disponible es limitado. 2) Por la misma razón, muchas de estas demostraciones son comprobadas y aprobadas por un número tan reducido de personas que no es raro encontrar errores o descuidos en sus comprobaciones.

La fruta colgante corta, es decir, los teoremas cortos y fáciles parecen haber sido ya demostrados, por lo que la mayoría de los que quedan son largos y penosos. Como físico, podría decir que las teorías formales (y a veces escandalosas por su informalidad) de la física no alcanzaron aún este nivel de complejidad. Mucho menos las otras ciencias.

Pero creo que el problema se solucionará en un futuro no muy lejano. Una vez que podamos construir sistemas de pruebas fiables en ordenadores lo suficientemente rápidos, la corrección de la mayoría de las pruebas no la decidirán los humanos, sino un software matemático de IA muy avanzado.

Siento no haber incluido ejemplos concretos porque no soy matemático, pero por lo que he leído últimamente, es un tema importante en las matemáticas actuales.