En 1996, un problema abierto de larga data fue resuelto por una computadora; a saber, que el álgebra de Robbins y el álgebra booleana son lo mismo. La prueba fue encontrada por un probador de teoremas automatizado.
Además, la prueba conocida del teorema de cuatro colores contiene componentes generados por computadora.
El objetivo de esta pregunta es enumerar las pruebas que se encuentran (total o parcialmente) por computadora (ya sea la única prueba conocida o la descubierta por primera vez).
soft-question
big-list
proofs
automated-theorem-proving
Mahdi Cheraghchi
fuente
fuente
Respuestas:
Otro ejemplo famoso es la prueba de Hales de la conjetura de Kepler que tenía un componente muy grande asistido por computadora.
De Wikipedia :
fuente
Esto es más una meta respuesta ya que es una lista de listas.
Los papeles de Doron Zeilberger . Es matemático y su computadora figura en el coautor Shalosh B. Ekhad en todos los documentos en los que la computadora jugó un papel en la obtención de los resultados.
Obra de Georges Gonthier . Diseñó una prueba verificada a máquina del teorema de los cuatro colores y recientemente ha estado trabajando en el teorema de Feit-Thompson. Recientemente completó la formalización del Teorema del orden impar.
Archive of Formal Proofs contiene pruebas verificadas con Isabelle e incluye teoremas de corrección para algoritmos, el teorema de Gauss-Jordan, alguna teoría del orden, teoría de la categoría y muchos más resultados clásicos.
Formalizing 100 Theorems , contiene pruebas comprobadas a máquina de algunos teoremas famosos.
fuente
Un ejemplo es la prueba de la inexistencia de un plano proyectivo de orden 10 .
Consulte La búsqueda de un plano proyectivo finito de orden 10 y La inexistencia de planos proyectivos finitos de orden 10 .
fuente