¿Por qué el teorema automático es una tarea tan difícil para las computadoras?

Porque las pruebas importantes requieren una imaginación salvaje.

El trabajo más importante en matemáticas se realiza inventando una hermosa estructura, de la cual el teorema se descarta como un aparente efecto secundario. El instinto del matemático es hacia la elegancia, la percepción subjetiva de la belleza. El teorema en sí mismo hace poco para señalar el camino. La estructura, una vez descubierta, generalmente arroja cientos de teoremas más importantes y plantea conjeturas más importantes.

El trabajo en matemática no es la ruptura procesal de los teoremas; Es una exploración de un paisaje estructural e intrincado. De vez en cuando, un explorador aterriza en una costa distante y la atención se desplaza a un nuevo continente.

Por ejemplo, Evariste Galois abordó el problema de resolver polinomios por encima del grado 4. Creó, aparentemente de la nada, una elegante torre de ruedas girando dentro de las ruedas. Para polinomios de grado 5, no se puede hacer que las ruedas encajen entre sí y el motor se rompe.

Olvídese de resolver polinomios, el descubrimiento de Galois (teoría de grupos) fue una visión profunda de la simetría. Ahora está en todas partes en matemáticas y física, desde la cristalografía hasta la ruptura de códigos.

Para otro ejemplo, Godel consideró si alguna vez podemos estar seguros de tener suficientes axiomas para hacer la teoría de números. Su construcción fue tan salvaje que habría sido considerada una locura, si no hubiera funcionado. Gódel volvió las matemáticas para verse a sí mismo, se volvió “consciente de sí mismo” (para volverse poético). Esta “introspección” creó un punto ciego, una singularidad que el motor no podía ver.

La estructura se derrumbó.

El trabajo de Godel a menudo se cita como el teorema más bello e importante de las matemáticas, y abre a la puerta resultados más sorprendentes como el Axioma de Elección y la tesis de Church-Turing.

Los teoremas que vemos escritos por estos investigadores son como los registros de exploradores náuticos del barco; son las más simples anotaciones de las visiones más profundas que la mente humana ha vislumbrado.

(Betrand Russell bromeó, de un estudiante que abandonó las matemáticas por poesía, “Eso es bueno. Las matemáticas requieren demasiada imaginación para este tipo”. [Parafraseo, se necesita referencia])

(Los matemáticos, sin duda, objetarán mis simplificaciones aquí. Siento que descripciones como estas a veces tienen un propósito, y espero que esta respuesta sirva como una invitación a estos temas y no como un objetivo para, um, selección de liendres)

Porque no entendemos los procesos de demostración de teoremas. No solo no entendemos el proceso de prueba de teoremas, me parece que no sabemos lo que no sabemos, por lo que la pregunta “por qué es difícil” no puede responderse de manera útil.

Knuth escribió: “La ciencia es lo que entendemos lo suficientemente bien como para explicarlo a una computadora. El arte es todo lo demás que hacemos”. (Fuente: Prólogo de Don Knuth a A = B) La demostración del teorema es principalmente un arte en este momento. (¡Pero lea A = B! El libro A = B explica un algoritmo que prueba automáticamente una cierta clase de teoremas matemáticos, que superó lo que los humanos hicieron antes del algoritmo).

Las verdaderas razones no radican en la falta de creatividad, sino en la intratabilidad computacional de teorías lógicas interesantes.

En 1928, David Hilbert preguntó si había un algoritmo que para cualquier enunciado matemático pudiera decirnos si el enunciado es verdadero o falso. Esto se conoce como el problema Entscheidungs.

Sin embargo, incluso para teorías lógicas relativamente simples pero interesantes, se sabe desde hace tiempo que la verdad matemática es indecidible. Un resultado inicial importante es que este es el caso de la lógica de primer orden. Alonzo Church y Alan Turing demostraron esto a principios de la década de 1930: así comenzó su colaboración.

El hecho de que las teorías lógicas sean a menudo indecidibles es una muy buena razón por la cual es difícil demostrar el teorema automatizado.

Otra buena razón es que la búsqueda de pruebas puede tener una alta complejidad de tiempo. Para la lógica proposicional, una fórmula es demostrable si y solo si es una tautología. Lamentablemente, ni siquiera se sabe que el problema de la verificación de tautología sea NP-completo; una fórmula [math] \ varphi [/ math] es una tautología si [math] \ neg \ varphi [/ math] no es satisfactoria. En otras palabras, el problema de probabilidad es co-NP-hard.

Se ha trabajado mucho en la demostración de teoremas asistidos por computadora en los que se pueden verificar los pasos individuales de una prueba matemática. Si usamos este enfoque, depende de nosotros encontrar una idea para la prueba, pero podemos usar el asistente de prueba para ayudarnos a verificar la prueba formalizada e incluso a veces sugerir los siguientes pasos en la prueba.