¿Dónde y cómo ayudaron las computadoras a probar un teorema?

El propósito de esta pregunta es recopilar ejemplos de la informática teórica donde el uso sistemático de las computadoras fue útil.

1. al construir una conjetura que conduzca a un teorema,
2. falsificar un enfoque de conjetura o prueba,
3. construir / verificar (partes de) una prueba.

Si tiene un ejemplo específico, describa cómo se hizo. Quizás esto ayude a otros a usar las computadoras de manera más efectiva en su investigación diaria (que todavía parece ser una práctica poco común en TCS a partir de hoy).

(Marcado como wiki de la comunidad, ya que no existe una única respuesta "correcta").

Un ejemplo muy conocido es el Teorema de los cuatro colores , probado originalmente mediante una verificación exhaustiva.

Fija puntos en el plano. Sea T una triangulación (es decir, un gráfico de línea recta plana con los puntos como vértices que está completamente triangulado), y deje que el peso de la triangulación sea la suma de las longitudes de los bordes.$n$

Mostrar que el problema de la triangulación de peso mínimo (MWT) era NP-duro fue un problema abierto de larga data, dificultado por el hecho de que las longitudes de los bordes involucran raíces cuadradas, y la precisión deseada necesaria para calcularlas con precisión fue difícil de unir.

Mulzer y Rote demostraron que MWT era NP-hard , y en el proceso utilizaron asistencia informática para verificar la exactitud de sus dispositivos. Que yo sepa, no hay pruebas alternativas.

La prueba de Thomas Hales (su sitio, MathSciNet ) de la conjetura de Kepler implicó tanto análisis de casos, y los casos fueron verificados por computadora, que decidió intentar una prueba formal de ello. Su proyecto para hacerlo es FlysPecK , y estima que tomará 20 años de trabajo.

Los investigadores en lenguajes de programación usan regularmente pruebas asistidas por computadora en su trabajo, aunque no sé cuán esencial es esto en términos de su proceso de investigación (sin embargo, les impide escribir toneladas de manipulaciones tediosas).

Doron Zeilberger ha realizado algunos trabajos en el campo de las pruebas generadas por computadora. En particular, ha preparado un programa Maple para probar identidades geométricas , y otro programa para probar una clase de identidades combinatorias . Algunos de los métodos se mencionan en el libro A = B .

Las computadoras también se han utilizado para determinar los límites superiores en los tiempos de ejecución de los programas de retroceso que resuelven problemas difíciles de NP, y construyen dispositivos para probar resultados de inaccesibilidad. Este y otros temas llenos de diversión te esperan en un breve ensayo (advertencia, autopromoción extrema por delante) titulado "Aplicación de la práctica a la teoría". Ver http://arxiv.org/abs/0811.1305

Dada esta buena lista, ¡parece que debería actualizar el documento!

Francisco Santos propuso recientemente un contraejemplo a la conjetura de Hirsch , importante para la programación lineal y la combinatoria poliédrica. La verificación por computadora se usó primero para establecer algunas de las propiedades requeridas del ejemplo, aunque luego se descubrieron argumentos sin la ayuda de potencia computacional, cf. La publicación del blog de Gil Kalai o el artículo sobre arxiv .

No he visto esto mencionado aquí, pero un probador de teoremas automatizado resolvió el problema abierto de larga data de si las álgebras de Robbins son booleanas:

http://www.cs.unm.edu/~mccune/papers/robbins/

Esto es especialmente notable porque la computadora desarrolló la prueba completa y el problema había estado abierto durante varias décadas.

No estoy completamente seguro si califica como TCS, pero podría decirse que está estrechamente relacionado.

El algoritmo Karloff-Zwick para MAX-3SAT logra el rendimiento esperado 7/8. Sin embargo, el análisis se basa en desigualdades de volumen esférico no comprobadas. Estas desigualdades finalmente se confirmaron mediante pruebas asistidas por computadora en otro documento de Zwick .

Además de la prueba de Hales de la conjetura de Kepler como se mencionó anteriormente, la prueba de la conjetura de Honeycomb y la de la conjetura del Dodecaédrico también son asistidas por computadora.

Puede consultar la página de inicio de Shalosh B. Ekhad . Esta computadora ha estado publicando documentos por un tiempo (generalmente con coautores).

Christian Urban utilizó el asistente de pruebas Isabelle para verificar que uno de los principales teoremas de su tesis doctoral era en realidad un teorema [1]. Usando el asistente, se necesitaban hacer algunos cambios, pero el resultado prácticamente se mantuvo.

Del mismo modo, Urban y Narboux también descubrieron errores en una prueba de lápiz y papel de la prueba de integridad de Crary para la verificación de equivalencia.

Meikle y Fleuriot formalizaron el Grundlagen de Hilbert en Isabelle y demostraron que, contrariamente a las afirmaciones de Hilbert, todavía confiaba en su intuición para formalizar la geometría de manera axiomática (IIRC había agujeros en su prueba derivados de Hilbert asumiendo cosas sobre diagramas) [3] .

[1]: Revisitando la eliminación de cortes: una prueba difícil es realmente una prueba

[2]: Formalización en la prueba de integridad de Nominal Isabelle Crary para la verificación de equivalencia

[3]: Formalización del Grundlagen de Hilbert en Isabelle / Isar

Los resultados en " La geometría de los árboles de búsqueda binarios " de Demaine, Harmon, Iacono, Kane y Patraşcu se desarrollaron con la ayuda de un software para probar varios esquemas de carga y construir asnos óptimos para pequeñas secuencias de acceso. (Y sí, "asnos" es el término correcto).

N. Shankar verificó (completa y mecánicamente) la prueba de Godel del teorema de incompletitud y el teorema de la Iglesia - Rosser utilizando el probador del teorema de Boyer - Moore. Hay un libro que describe cómo se hizo.

Según Simon Plouffe , se descubrió la fórmula del algoritmo Bailey-Borwein-Plouffe para calcular el enésimo bit de Pi sin calcular ninguno de los bits más significativos , utilizando sistemas a prueba de computadora.

Existen numerosos ejemplos en el análisis de casos promedio de algoritmos. Quizás algunos de los primeros son los experimentos de computadora que llevaron al documento "Algunos resultados inesperados de comportamiento esperado para el embalaje de contenedores" por Bentley, Johnson, Leighton, McGeoch y McGeoch en STOC 1984.