¿Se ha demostrado algún resultado previamente desconocido mediante un probador de teoremas automatizado?

Question

El Página de Wikipedia sobre la demostración automática de teoremas estados:

A pesar de estos límites teóricos, en la práctica, los demostradores de teoremas pueden resolver muchos problemas difíciles...

Sin embargo, no está claro si estos "problemas difíciles" son nuevos. ¿Aportan las pruebas generadas por ordenador algo a las matemáticas "generadas por el hombre"?

Conozco el teorema de los cuatro colores, pero como se menciona en la página de Wikipedia, quizá sea más un ejemplo de verificación de pruebas que de razonamiento automatizado. Pero, ¿tal vez sea el mejor ejemplo?

Answer 1

Otro ejemplo sería probablemente la conjetura de Kepler, demostrada por un equipo en torno a Tomas Hales. Se llamaba Proyecto Flyspeck. Aunque afirmaba haberla demostrado antes, la gente no estaba segura de que la prueba fuera correcta. Así que esto podría entrar en la categoría de "comprobación de pruebas".

Answer 2

Ken Kunen tiene algunos trabajos sobre bucles en los que los resultados originales fueron demostrados por el prover de teoremas. Tiene este programa de probar primero los resultados de esta manera y luego analizar el resultado para obtener una buena prueba comprensible para los humanos.

Answer 3

Bob Veroff tiene algunos ejemplos de resultados que creo que muchos encontrarían interesantes, demostrados por primera vez por un ordenador, como las bases de axiomas simples relativamente cortas para el Álgebra de Boole. Sin embargo, no todo lo que demuestra allí constituye un nuevo resultado.

Un ejemplo quizás mejor consiste en la prueba de XCB como uno de los axiomas simples más cortos para el cálculo equivalencial clásico bajo el desprendimiento de E (de, E $\alpha$$ \N-beta $, as well as $ \N - Alfa $, we may infer $ \beta$). La prueba de XCB, en efecto, completó la solución de lo que se podría considerar como el problema mayor. El problema mayor aquí se puede enunciar como:

"Encuentra todo de los axiomas más cortos, hasta el reencaminamiento de variables, bajo el desprendimiento E para el cálculo equivalencial clásico".

Muchos problemas similares de mayor envergadura en lógica (y probablemente también el álgebra abstracta) siguen abiertos. Observo que el sitio de Ulrich no tiene una lista completa de estos problemas (esto no es para culpar a Ulrich)... por ejemplo el problema de encontrar el conjunto de los axiomas simples más cortos para el cálculo proposicional clásico en la disyunción "A", y la negación "N" bajo el desprendimiento A-N "De AN $\alpha$$ \N-beta $, as well as $ \N - Alfa $, infer $ \beta$", sigue abierto.

Answer 4

7 años después

Soy consciente de que algunos importantes ( $\color{red}{\text{named})}$ problemas matemáticos han tenido sus pruebas verificadas ( $\color{red}{\text{-or had been proven})}$ utilizando programas informáticos automatizados de demostración de teoremas o de ayuda a la demostración. Por ejemplo a La prueba de Feit y Thompson del teorema de impar-Orden ha sido verificada por la ayuda de la prueba COQ. Y este repositorio Git La demostración formal del Teorema del Orden impar, reposiciona el código, escrito en COQ y pone a disposición del público para reproducir los resultados . Subiendo por el directorio de archivos encuentro varios otros resultados: ( 1 ) Una prueba formal de la irracionalidad de $\zeta(3),$ La constante de Apery y ( 2 ) Prueba formal del teorema de los cuatro colores .