¿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

La conjetura de Robbins de que todo Álgebras de Robbins son álgebras booleanas se demostró por primera vez utilizando EQP Después de que Tarski y otros intentaran demostrarlo o refutarlo sin éxito.

Answer 2

Comprueba Resumen de nuevos resultados en matemáticas obtenidos con el software de deducción automatizada de Argonne . Enumera muchos problemas resueltos (aunque es una página antigua, resume los resultados obtenidos hasta 1995).

Algunas informaciones son también ici , sección ¿Para qué ha sido realmente útil la demostración automática de teoremas? .

Answer 3

La conjetura de Robbins, que ya se ha mencionado, es probablemente el ejemplo más interesante de lo que ya son capaces los demostradores automatizados de teoremas. Otro dato interesante que recuerdo es que el programa Logic Theorist de mediados de los cincuenta fue capaz de demostrar gran parte de los Principia Mathematica por sí mismo e incluso consiguió encontrar una demostración más elegante para el Teorema del Triángulo Isósceles que el propio Russell.

Sin embargo, me gustaría aclarar lo que has dicho sobre el Teorema de los Cuatro Colores: a lo que se refiere la Wikipedia es a la demostración de este teorema utilizando Coq, que es un probador de teoremas interactivo. La idea básica es que el usuario proporciona una demostración paso a paso y el demostrador de teoremas demuestra la validez de cada paso por sí mismo. Los diferentes demostradores de teoremas tienen diferentes niveles de automatización; el único que conozco es Isabelle, que tiene una automatización bastante potente. Un ejemplo notable es el teorema de Cantor de que no existe un mapeo inyectivo de un conjunto a su conjunto de potencias, que puede demostrarse de forma completamente automática mediante uno de los muchos métodos de demostración de Isabelle. Sin embargo, esto es más o menos una coincidencia, el sistema normalmente no puede demostrar teoremas como este por sí mismo, pero maneja cosas como simplificaciones tediosas y distinciones de casos bastante bien y a veces resuelve problemas que no son inmediatamente obvios para mí de forma automática. Por desgracia, la mayoría de las veces ocurre lo contrario.

Answer 4

Recientemente, yo y muchos colegas hemos estado demostrando teoremas de combinatoria sobre palabras utilizando el prover de Walnut escrito por Hamoon Mousavi. Algunos de estos teoremas no son triviales y para algunos no se conoce ninguna otra prueba. También se ha utilizado para corregir resultados ligeramente erróneos en la literatura.

Para más información sobre la nuez, consulte https://arxiv.org/abs/1603.06017 .

Para ver algunos de mis artículos sobre este tema, consulte https://cs.uwaterloo.ca/~shallit/papers.html .

Answer 5

Google para esto " demostración automatizada de teoremas en el diseño de hardware "(sin las comillas). Hay muchos resultados interesantes, que muestran el uso de la demostración automatizada de teoremas para el diseño de hardware. El teorema sería entonces algo así como "El diseño X verifica las propiedades especificadas", ciertamente un teorema interesante a su manera, pero tal vez no lo que el PO pensó.