¿Por qué es tan difícil para una computadora probar algo?

18

Esto puede considerarse una pregunta estúpida. No soy un experto en informática (y tampoco soy matemático), así que discúlpeme si cree que las siguientes preguntas muestran algunos supuestos erróneos importantes.

Si bien hay planes para formalizar el último teorema de Fermat (ver esta presentación ), nunca he leído ni escuchado que una computadora pueda probar incluso un teorema "simple" como el de Pitágoras.

Por qué no? ¿Cuál es (/ son) la principal dificultad (s) detrás de establecer una prueba totalmente autónoma por una computadora, ayudada solo por algunos "axiomas incorporados"?

Una segunda pregunta que me gustaría hacer es la siguiente: ¿Por qué podemos formalizar muchas pruebas, mientras que actualmente es imposible que una computadora pruebe un teorema por sí misma? ¿Por qué es eso "más difícil"?

Max Muller
fuente
77
Dos dificultades principales. Incompletez (ver Teoremas de Gödel) y el gran tamaño del espacio de búsqueda (hay muchos más teoremas poco interesantes que interesantes). Se han realizado progresos considerables utilizando asistentes de prueba (Coq, Isabelle, Agda, etc.). Con estos, el matemático escribe los teoremas y lemas y el asistente de pruebas ayuda a encontrar pruebas y asegura que las pruebas sean lógicamente válidas.
Dave Clarke
@Dave Clarke: ok, entonces en realidad dices que una computadora es capaz de probar (nuevos) teoremas, pero la gran cantidad de búsquedas posibles le dificulta a él / ella / ella escribir un teorema que tenga algún valor o sea interesante, estoy en lo cierto? ¿Podría explicar por qué los teoremas de Gödel y la "incompletitud" son relevantes aquí? Además, ¿tiene una referencia de un trabajo de investigación o artículo de encuesta en el que se demuestre que una computadora realmente demuestra un teorema? Por último, ¿se está investigando mucho para intentar que las computadoras prueben teoremas? ¿Cómo se llama esta área de investigación (cont ...)
Max Muller
y conoces buen material introductorio? ¿Cuáles son los requisitos previos en matemáticas, pero especialmente en Ciencias de la Computación para comprender realmente este material?
Max Muller
77
Puede que le interese parte del trabajo de Dorian Zeilberger, como "¡ Enseñando a la computadora a descubrir (!) Y luego a probar (!!) (todo por sí mismo (!!!)) análogos de la conjetura notoria 3x + 1 de Collatz " ( math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/collatz.html ). El coautor frecuente de Zeilberger, Shalosh B. Ekhad, es una computadora.
Rob Simmons
44
La siguiente pregunta también ofrece varios buenos ejemplos de computadoras que ayudan a probar teoremas: cstheory.stackexchange.com/questions/82/…
Mugizi Rwebangira

Respuestas:

22

Si bien hay planes para formalizar el último teorema de Fermat (ver esta presentación), nunca he leído ni escuchado que una computadora pueda probar incluso un teorema "simple" como el de Pitágoras.

En 1949, Tarski demostró que casi todo en The Elements se encuentra dentro de un fragmento de lógica decidible, cuando mostró la capacidad de decisión de la teoría de primer orden de los campos cerrados reales. Entonces, el teorema de Pitágoras en particular no se habla mucho porque no es especialmente difícil.

UNUN

UNsiUN

Neel Krishnaswami
fuente
18

Dos dificultades principales. Incomplete (ver Teoremas de incompletitud de Gödel) y el gran tamaño del espacio de búsqueda (hay muchos más teoremas poco interesantes que interesantes). Se han realizado progresos considerables utilizando asistentes de prueba ( Coq , Isabelle, Agda, etc.). Con estos, el matemático escribe los teoremas y lemas y el asistente de pruebas ayuda a encontrar pruebas y asegura que las pruebas sean lógicamente válidas.

PAGQPAGQ

Este artículo describe cómo se utiliza el asistente de pruebas Coq para probar el teorema de los cuatro colores. La matemática mecanizada ( descripción general ) es un área de TCS dedicada a (semi) probar automáticamente teoremas (y en general usar computadoras para ayudar a los matemáticos).

Un área en la que la demostración automatizada de teoremas (más o menos) está teniendo un impacto es en la verificación y la búsqueda de modelos. La verificación de modelos trata de determinar si un sistema determinado satisface una propiedad determinada, mientras que la búsqueda de modelos encuentra un sistema para satisfacer una colección de propiedades dada. La herramienta Alloy emplea la verificación de modelos y la búsqueda de modelos con buenos resultados, y es bastante útil.

Dave Clarke
fuente
No pude elegir entre estas dos respuestas, porque ambas son geniales. Lancé una moneda para decidir cuál elegir. Lo siento, no elegí el tuyo! Muchas gracias de todos modos.
Max Muller
A veces se gana, se pierde algo.
Dave Clarke
Una descripción menos técnica y más matemática de las cuatro pruebas de color y su importancia se publicó en un reciente número de avisos de AMS (todo el tema podría ser una lectura aconsejable para las personas interesadas en la pregunta del OP).
Francois G