Prueba asistida por computadora

Prueba matemática al menos parcialmente generada por computadora

Una prueba asistida por computadora es una prueba matemática que ha sido generada al menos parcialmente por computadora .

La mayoría de las demostraciones asistidas por computadora hasta la fecha han sido implementaciones de grandes demostraciones por agotamiento de un teorema matemático . La idea es utilizar un programa informático para realizar cálculos extensos y proporcionar una prueba de que el resultado de estos cálculos implica el teorema dado. En 1976, el teorema de los cuatro colores fue el primer teorema importante que se verificó utilizando un programa informático .

También se han hecho intentos en el área de investigación de inteligencia artificial para crear nuevas pruebas más pequeñas y explícitas de teoremas matemáticos desde abajo hacia arriba utilizando técnicas de razonamiento automatizado como la búsqueda heurística . Estos demostradores de teoremas automatizados han demostrado una serie de nuevos resultados y han encontrado nuevas pruebas para teoremas conocidos. ^{[ cita requerida ]} Además, los asistentes de prueba interactivos permiten a los matemáticos desarrollar pruebas legibles para humanos que, no obstante, se verifican formalmente para comprobar su corrección. Dado que estas pruebas son generalmente examinables por humanos (aunque con dificultad, como en el caso de la prueba de la conjetura de Robbins ), no comparten las controvertidas implicaciones de las pruebas por agotamiento asistidas por computadora.

Métodos

Un método para utilizar computadoras en demostraciones matemáticas es por medio de los llamados cálculos numéricos validados o cálculos numéricos rigurosos. Esto significa calcular numéricamente pero con rigor matemático. Se utiliza la aritmética de valores conjuntos y el principio de inclusión ^{[ aclarar ]} para asegurar que la salida de valores conjuntos de un programa numérico encierra la solución del problema matemático original. Esto se hace controlando, encierra y propagando errores de redondeo y truncamiento utilizando, por ejemplo, la aritmética de intervalos . Más precisamente, se reduce el cálculo a una secuencia de operaciones elementales, por ejemplo . En una computadora, el resultado de cada operación elemental se redondea por la precisión de la computadora. Sin embargo, se puede construir un intervalo proporcionado por límites superiores e inferiores en el resultado de una operación elemental. Luego se procede reemplazando números con intervalos y realizando operaciones elementales entre dichos intervalos de números representables. ^{[ cita requerida ]} ${\displaystyle (+,-,\times ,/)}$

Objeciones filosóficas

Las demostraciones asistidas por ordenador son objeto de cierta controversia en el mundo matemático, y Thomas Tymoczko fue el primero en formular objeciones. Quienes se adhieren a los argumentos de Tymoczko creen que las demostraciones asistidas por ordenador que requieren mucho tiempo no son, en cierto sentido, demostraciones matemáticas "reales", porque implican tantos pasos lógicos que no son verificables en la práctica por seres humanos, y que en realidad se les pide a los matemáticos que sustituyan la deducción lógica a partir de axiomas supuestos por la confianza en un proceso computacional empírico, que puede verse afectado por errores en el programa informático, así como por defectos en el entorno de ejecución y en el hardware. ^[1]

Otros matemáticos creen que las demostraciones asistidas por computadora deben considerarse cálculos , en lugar de demostraciones : el algoritmo de demostración en sí mismo debe demostrar su validez, de modo que su uso pueda considerarse entonces como una mera "verificación". Los argumentos de que las demostraciones asistidas por computadora están sujetas a errores en sus programas fuente, compiladores y hardware pueden resolverse proporcionando una prueba formal de corrección para el programa de computadora (un enfoque que se aplicó con éxito al teorema de los cuatro colores en 2005) así como replicando el resultado utilizando diferentes lenguajes de programación, diferentes compiladores y diferente hardware de computadora.

Otra forma posible de verificar las pruebas asistidas por computadora es generar sus pasos de razonamiento en un formato legible por máquina y luego usar un programa de verificación de pruebas para demostrar su corrección. Dado que validar una prueba dada es mucho más fácil que encontrar una prueba, el programa de verificación es más simple que el programa asistente original y, en consecuencia, es más fácil ganar confianza en su corrección. Sin embargo, este enfoque de usar un programa de computadora para demostrar que el resultado de otro programa es correcto no atrae a los escépticos de las pruebas por computadora, quienes lo ven como agregar otra capa de complejidad sin abordar la necesidad percibida de comprensión humana.

Otro argumento contra las demostraciones asistidas por computadora es que carecen de elegancia matemática , es decir, que no aportan ninguna información o conceptos nuevos y útiles. De hecho, este es un argumento que podría esgrimirse contra cualquier demostración extensa por agotamiento.

Una cuestión filosófica adicional que plantean las demostraciones asistidas por ordenador es si convierten las matemáticas en una ciencia cuasi-empírica , donde el método científico se vuelve más importante que la aplicación de la razón pura en el área de conceptos matemáticos abstractos. Esto se relaciona directamente con el debate dentro de las matemáticas sobre si las matemáticas se basan en ideas o son "simplemente" un ejercicio de manipulación formal de símbolos. También plantea la cuestión de si, según la visión platónica , todos los objetos matemáticos posibles en algún sentido "ya existen", si las matemáticas asistidas por ordenador son una ciencia observacional como la astronomía, en lugar de una ciencia experimental como la física o la química. Esta controversia dentro de las matemáticas se está produciendo al mismo tiempo que se están planteando preguntas en la comunidad de la física sobre si la física teórica del siglo XXI se está volviendo demasiado matemática y está dejando atrás sus raíces experimentales.

El campo emergente de las matemáticas experimentales está afrontando este debate de frente centrándose en los experimentos numéricos como su principal herramienta de exploración matemática.

Teoremas demostrados con ayuda de programas informáticos

La inclusión en esta lista no implica que exista una prueba formal verificada por computadora, sino que se ha involucrado un programa informático de alguna manera. Consulte los artículos principales para obtener más detalles.

• Teorema de los cuatro colores , 1976 ^[2]
• Conjetura de universalidad de Mitchell Feigenbaum en dinámica no lineal. Demostrada por OE Lanford mediante aritmética computacional rigurosa, 1982
• Connect Four , 1988: un juego resuelto
• Inexistencia de un plano proyectivo finito de orden 10, 1989
• Conjetura de la doble burbuja , 1995 ^[3]
• Conjetura de Robbins , 1996
• Conjetura de Kepler , 1998: el problema del empaquetamiento óptimo de esferas en una caja
• Atractor de Lorenz , 2002 – 14.º de los problemas de Smale demostrados por Warwick Tucker mediante aritmética de intervalos
• Caso de 17 puntos del problema del final feliz , 2006
• Kouril ^{[4] [5] [6]} (entre 2006 y 2016) calculó varios números de van der Waerden utilizando un solucionador SAT basado en FPGA .
• Dureza NP de la triangulación de peso mínimo , 2008
• Ahmed ^{[7] [8] [9] [10] [11]} (entre 2009 y 2014) calculó varios números de van der Waerden utilizando solucionadores SAT independientes y distribuidos basados ​​en el algoritmo DPLL . Ahmed utilizó por primera vez solucionadores SAT distribuidos por grupos para demostrar que w(2; 3, 17) = 279 y w(2; 3, 18) = 312 en 2010. ^[8]
• Las soluciones óptimas para el cubo de Rubik se pueden obtener con un máximo de 20 movimientos de caras, 2010 ^[12]
• El número mínimo de pistas para resolver un sudoku es 17, 2012
• En 2014 se resolvió un caso especial del problema de discrepancia de Erdős utilizando un solucionador SAT . La conjetura completa fue resuelta más tarde por Terence Tao sin asistencia informática. ^[13]
• Problema de triples pitagóricos booleanos resuelto utilizando 200 terabytes de datos en mayo de 2016. ^[14]
• Aplicaciones de la teoría de Kolmogorov-Arnold-Moser ^{[15] [16]}
• Propiedad de Kazhdan (T) para el grupo de automorfismos de un grupo libre de rango al menos cinco
• El número cinco de Schur , la prueba de que S(5) = 161 fue anunciada en 2017 por Marijn Heule y ocupó 2 petabytes de espacio ^{[17] [18]}
• La conjetura de Keller en dimensión 7 es el único caso restante en 2020 con una prueba de 200 gigabytes ^{[19] [20]}
• El número cromático de empaquetamiento de la cuadrícula cuadrada infinita es 15, según Subercaseaux y Heule en 2023 ^{[21] [22]} (Véase también: Problema de Hadwiger–Nelson para el número cromático del plano)
• Existencia de funciones conmutativas sin punto fijo común, 1967 ^[23]

Véase también

• Verificación formal
• Teórico de la lógica
• Prueba matemática
• Metamatemáticas
• Comprobación de modelos
• Diecisiete o nada
• Computación simbólica
• Números validados

Referencias

1. Tymoczko, Thomas (1979), "El problema de los cuatro colores y su importancia matemática", The Journal of Philosophy , 76 (2): 57–83, doi :10.2307/2025976, JSTOR  2025976.
2. Gonthier, Georges (2008), "Demostración formal: el teorema de los cuatro colores" (PDF) , Notices of the American Mathematical Society , 55 (11): 1382–1393, MR  2463991, archivado (PDF) desde el original el 2011-08-05
3. Hass, J.; Hutchings, M.; Schlafly, R. (1995). "La conjetura de la doble burbuja". Anuncios electrónicos de investigación de la American Mathematical Society . 1 (3): 98–102. CiteSeerX 10.1.1.527.8616 . doi :10.1090/S1079-6762-95-03001-0. 
4. Kouril, Michal (2006). Un marco de trabajo de seguimiento hacia atrás para clústeres Beowulf con una extensión a la computación multiclúster y la implementación del problema de referencia Sat (tesis doctoral). Universidad de Cincinnati.
5. Kouril, Michal (2012). "Cálculo del número de van der Waerden W(3,4)=293". Enteros . 12 : A46. MR  3083419.
6. Kouril, Michal (2015). "Aprovechamiento de clústeres FPGA para cálculos SAT". Computación paralela: en el camino hacia la exaescala : 525–532.
7. Ahmed, Tanbir (2009). "Algunos números nuevos de van der Waerden y algunos números tipo van der Waerden". Enteros . 9 : A6. doi :10.1515/integ.2009.007. SEÑOR  2506138. S2CID  122129059.
8. Ahmed, Tanbir (2010). "Dos nuevos números de van der Waerden w(2;3,17) y w(2;3,18)". Enteros . 10 (4): 369–377. doi :10.1515/integ.2010.032. SEÑOR  2684128. S2CID  124272560.
9. Ahmed, Tanbir (2012). "Sobre el cálculo de números de van der Waerden exactos". Enteros . 12 (3): 417–425. doi :10.1515/integ.2011.112. MR  2955523. S2CID  11811448.
10. Ahmed, Tanbir (2013). "Algunos números más de Van der Waerden". Revista de secuencias enteras . 16 (4): 13.4.4. MR  3056628.
11. Ahmed, Tanbir; Kullmann, Oliver; Snevily, Hunter (2014). "Sobre los números de van der Waerden w(2;3,t)". Matemáticas Aplicadas Discretas . 174 (2014): 27–51. arXiv : 1102.5433 . doi : 10.1016/j.dam.2014.05.007 . MR  3215454.
12. "El número de Dios es 20". cube20.org . Julio de 2010 . Consultado el 18 de octubre de 2023 .
13. Cesare, Chris (1 de octubre de 2015). «Un genio de las matemáticas resuelve el acertijo de un maestro». Nature . 526 (7571): 19–20. Bibcode :2015Natur.526...19C. doi : 10.1038/nature.2015.18441 . PMID  26432222.
14. Lamb, Evelyn (26 de mayo de 2016). «La prueba matemática de doscientos terabytes es la más grande jamás realizada». Nature . 534 (7605): 17–18. Bibcode :2016Natur.534...17L. doi : 10.1038/nature.2016.19990 . PMID  27251254.
15. Celletti, A.; Chierchia, L. (1987). "Estimaciones rigurosas para una teoría KAM asistida por computadora". Journal of Mathematical Physics . 28 (9): 2078–86. Bibcode :1987JMP....28.2078C. doi :10.1063/1.527418.
16. Figueras, JL; Haro, A.; Luque, A. (2017). "Aplicación rigurosa asistida por ordenador de la teoría KAM: un enfoque moderno". Fundamentos de las matemáticas computacionales . 17 (5): 1123–93. arXiv : 1601.00084 . doi :10.1007/s10208-016-9339-3. hdl :2445/192693. S2CID  28258285.
17. Heule, Marijn JH (2017). "Schur número cinco". arXiv : 1711.08076 [cs.LO].
18. "Schur número cinco". www.cs.utexas.edu . Consultado el 6 de octubre de 2021 .
19. Brakensiek, Josué; Heule, Marijn; Mackey, Juan; Narváez, David (2020). "La resolución de la conjetura de Keller". En Peltier, Nicolás; Sofronie-Stokkermans, Viorica (eds.). Razonamiento automatizado . Apuntes de conferencias sobre informática. vol. 12166. Saltador. págs. 48–65. doi :10.1007/978-3-030-51074-9_4. ISBN 978-3-030-51074-9. Número de pieza  7324133 .
20. Hartnett, Kevin (19 de agosto de 2020). "Computer Search resuelve un problema matemático de hace 90 años". Quanta Magazine . Consultado el 8 de octubre de 2021 .
21. Subercaseaux, Bernardo; Heule, Marijn JH (23 de enero de 2023). "El número cromático de empaquetamiento de la cuadrícula cuadrada infinita es 15". arXiv : 2301.09757 [cs.DM].
22. Hartnett, Kevin (20 de abril de 2023). "El número 15 describe el límite secreto de una cuadrícula infinita". Revista Quanta . Consultado el 20 de abril de 2023 .
23. Boyce, William M. "Funciones conmutativas sin punto fijo común" (PDF) . American Mathematical Society . Transactions of the American Mathematical Society . Consultado el 31 de agosto de 2024 .

Lectura adicional

• Lenat, DB (1976). AM: Un enfoque de inteligencia artificial para el descubrimiento en matemáticas como búsqueda heurística (PDF) (PhD). AI Lab., Stanford University. STAN-CS-76-570, Informe del proyecto de programación heurística HPP-76-8.
• Meyer, KR; Schmidt, DS, eds. (2012). Pruebas asistidas por computadora en análisis. Volúmenes de IMA en matemáticas y sus aplicaciones. Vol. 28. Springer. ISBN 978-1-4613-9092-3.
• Nakao, M.; Plum, M.; Watanabe, Y. (2019). Métodos de verificación numérica y pruebas asistidas por computadora para ecuaciones diferenciales parciales. Springer Series in Computational Mathematics. Springer. ISBN 9789811376696.

Enlaces externos

• Lanford, Oscar E. (1982). "Una prueba asistida por computadora de las conjeturas de Feigenbaum" (PDF) . Bull. Amer. Math. Soc . 6 (3): 427–434. CiteSeerX  10.1.1.434.8389 . doi :10.1090/S0273-0979-1982-15008-X.
• Furse, Edmund (1990). ¿Por qué la AM perdió fuelle? (Informe técnico). Departamento de Estudios Informáticos, Universidad de Glamorgan. CS-90-4. Archivado desde el original el 17 de julio de 2012. Consultado el 6 de septiembre de 2016 .{{cite tech report}}: CS1 maint: bot: estado de URL original desconocido ( enlace )
• Begley, S. (16 de abril de 2018). "Las pruebas numéricas realizadas por computadora pueden ser erróneas". Pittsburgh Post-Gazette . Archivado desde el original el 16 de abril de 2018.
• "Número especial sobre la demostración formal". Avisos de la American Mathematical Society . Diciembre de 2008.