Prueba asistida por ordenador

"Averiguar si cualquier mapa se puede pintar con cuatro colores, de forma que cualquier par de regiones contiguas estén pintadas de diferentes colores". En 1976, K. Appel y V. Haken, con la ayuda de cálculos de ordenador diseñados al efecto, demostraron que es posible colorear cualquier mapa con cuatro colores

Una prueba asistida por ordenador es una demostración matemática que ha sido generada al menos parcialmente utilizando una computadora.

La mayoría de las pruebas asistidas por ordenador hasta la fecha han sido desarrollos de pruebas por exhaustación de un elevado número de casos asociados a un teorema matemático. La idea es usar un programa de computadora para realizar cálculos largos 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ó con un programa informático.

También se han realizado intentos en el área de investigación de la inteligencia artificial para crear pruebas más pequeñas, explícitas y nuevas de teoremas matemáticos de abajo hacia arriba usando técnicas de razonamiento automático, como la búsqueda heurística. Tales demostraciones automáticas de teoremas han demostrado numerosos nuevos resultados y han encontrado nuevas pruebas para teoremas conocidos. Además, la demostración interactiva de teoremas permite a los matemáticos desarrollar pruebas legibles para los seres humanos que, no obstante, se verifican formalmente para verificar su exactitud. Dado que estas pruebas son generalmente revisables por los matemáticos (aunque no sin dificultades, como con la prueba de la conjetura de Robbins) no comparten las implicaciones controvertidas de las pruebas asistidas por ordenador mediante agotamiento.

Métodos

Un método para usar computadoras en pruebas matemáticas es por medio de los sistemas denominados validación numérica o rigor numérico. Esto significa calcular numéricamente, pero con rigor matemático. Se usa de principios aritméticos y la inclusión con valores establecidos para garantizar que la salida de valor fijo de un programa numérico encierre la solución del problema matemático original. Esto se hace controlando, adjuntando y propagando los errores de redondeo y truncamiento usando, por ejemplo, intervalos aritméticos. Más precisamente, si se reduce el cálculo a una secuencia de operaciones elementales, como (+, -, *, /). En una computadora, el resultado de cada operación elemental se completa con su precisión de cálculo. Sin embargo, puede construirse un intervalo proporcionado por límites superiores e inferiores sobre el resultado de una operación elemental. A continuación se procede reemplazando números por intervalos y realizando operaciones elementales entre dichos intervalos de números representables.

Objeciones filosóficas

Las pruebas asistidas por ordenador son objeto de cierta controversia en el mundo de las matemáticas, siendo Thomas Tymoczko uno de los primeros en formular objeciones. Aquellos que se adhieren a los argumentos de Tymoczko creen que las largas pruebas asistidas por ordenador no son, en cierto sentido, demostraciones reales porque implican tantos pasos lógicos que no son prácticamente verificables por los seres humanos, y que se está pidiendo a los matemáticos que reemplacen de forma efectiva la deducción lógica de axiomas asumidos por la confianza en un proceso computacional empírico, que se ve potencialmente afectado por errores en el programa de la computadora, así como también por defectos en el entorno de tiempo de ejecución y del propio dispositivo.​

Otros matemáticos creen que las largas pruebas asistidas por computadora deben considerarse como cálculos, en lugar de pruebas: el algoritmo de prueba en sí mismo debe probarse como válido, de modo que su uso puede considerarse como una mera verificación. Los argumentos de que las pruebas asistidas por ordenador están sujetas a errores en sus programas fuente, compiladores y dispositivos electrónicos pueden resolverse proporcionando una prueba formal de corrección del programa informático (un enfoque que se aplicó con éxito al teorema de los cuatro colores en 2005), así como replicar el resultado usando diferentes lenguajes de programación, diferentes compiladores y diferentes tipos de computadora.

Otra forma posible de verificar las pruebas asistidas por ordenador es generar sus pasos de razonamiento en una forma legible por una máquina, y luego usar una demostración automática de teoremas para comprobar su corrección. Este enfoque de usar un programa de computadora para probar que otro programa es correcto no atrae a los escépticos de las pruebas con ordenador, que lo ven como una capa de complejidad añadida sin abordar la necesidad percibida de la comprensión humana.

Otro argumento en contra de las pruebas asistidas por ordenador es que carecen de belleza matemática, que no proporcionan ideas ni conceptos nuevos y útiles. De hecho, este es un argumento que podría avanzarse contra cualquier prueba prolongada por agotamiento.

Una cuestión filosófica adicional planteada por las pruebas asistidas por ordenador es si convierten las matemáticas en una ciencia cuasi-empírica, en la que el método científico se vuelve más importante que la aplicación de la razón pura en el área de los conceptos matemáticos abstractos. Esto se relaciona directamente con el argumento dentro de las matemáticas sobre si las matemáticas se basan en ideas, o simplemente son un ejercicio de manipulación de símbolos formales. También plantea la cuestión de si, de acuerdo con el punto de vista platónico, 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 experimental como la física o la química. Curiosamente, esta controversia dentro de las matemáticas está ocurriendo al mismo tiempo que las preguntas que se hacen en la comunidad de la física sobre si la física teórica del siglo veintiuno se está volviendo demasiado matemática y está dejando atrás sus raíces experimentales.

El campo emergente de las matemáticas experimentales dilucida este debate de frente, al enfocarse en los experimentos numéricos como su herramienta principal para la exploración matemática.

Teoremas en venta

En 2010, los académicos de la Universidad de Edimburgo ofrecieron a las personas la posibilidad de "comprar su propio teorema" creado a través de una prueba asistida por ordenador. Este nuevo teorema llevaría el nombre del comprador.​​

Ejemplos

Teoría de números

Debido a que la teoría de números opera en gran medida con números enteros, el uso de cálculos basados en la evidencia en este campo resulta ser muy fructífera.

• Se afirma que el número de Mersenne $M_{43112609}=2^{43112609}-1$ es un número primo. Este hecho puede verificarse teóricamente mediante razonamientos humanos, pero de forma práctica solo con el uso de tecnología informática.
• Leonhard Euler formuló la conjetura de que la ecuación $x_{1}^{5}+x_{2}^{5}+x_{3}^{5}+x_{4}^{5}=x_{5}^{5}$ no tiene solución en números enteros positivos. Sin embargo, posteriormente se demostró que hay al menos una solución:

$x_{1}=27$, $x_{2}=84$, $x_{3}=110$, $x_{4}=133$, $x_{5}=144$. Esta solución se encontró usando un procedimiento de búsqueda de fuerza bruta por ordenador.​

Teoría de grafos

Uno de los éxitos más famosos en la aplicación de pruebas informáticas en teoría de grafos es la solución del teorema de los cuatro colores. Este famoso problema se planteó en 1852, y se formula de la siguiente manera: "Averiguar si cualquier mapa se puede pintar con cuatro colores, de forma que cualquier par de regiones contiguas estén pintadas de diferentes colores". En 1976, K. Appel y V. Haken, con la ayuda de cálculos diseñados al efecto, demostraron que es posible colorear cualquier mapa con cuatro colores.

Hidrodinámica

El Instituto Kéldysh de Matemática Aplicada convirtió la hidrodinámica en un objeto sistemático de investigación con el uso de cálculos asistidos por ordenador bajo la dirección de Konstantín Ivánovich Babenko. Un ejemplo es el siguiente teorema:.​

• Teorema: Cuando $\alpha =1.02$ y $R=6000$ el problema espectral de Orr-Sommerfeld tiene un valor propio que se encuentra en el semiplano $\mathrm {Re} \,\lambda >0$. En consecuencia, en la formulación lineal de estos parámetros, el flujo de Poiseuille es inestable.

Lista de teoremas probados con la ayuda de programas de ordenador

La inclusión en esta lista no implica que exista una prueba formal documentada por computadora, sino que un programa de ordenador ha estado involucrado de alguna manera en su demostración. Véanse los artículos principales para más detalles.

• Teorema de los cuatro colores, 1976
• Cálculos del caso mínimo de la cuadratura del cuadrado, descubierto por Arie Duijvestijn en 1978
• Conjetura de universalidad de Mitchell Feigenbaum en dinámica no lineal. Probado por O. E. Lanford usando una aritmética computarizada rigurosa, 1982
• Conecta 4, 1988 - un juego resuelto
• No existencia de un plano proyectivo finito de orden 10, 1989
• Conjetura de Robbins, 1996
• Conjetura de Kepler, 1998 - el problema del embalaje óptimo de la esfera en una caja
• Atractor de Lorenz, 2002 - el Problemas de Smale número 14 probado por W. Tucker usando aritmética de intervalos
• Caso de 17 puntos del Problema del final feliz, 2006
• Computabilidad NP de la triangulación de peso mínimo, 2008
• Las soluciones óptimas del Cubo de Rubik se puede obtener en un máximo de 20 movimientos de cara, 2010
• El número mínimo de pistas para un Sudoku resoluble es de 17, 2012
• En 2014, se resolvió un caso especial del problema de la discrepancia de Erdős utilizando un problema de satisfacibilidad booleana. La conjetura completa fue luego resuelta por Terence Tao sin la ayuda de una computadora.​
• Problema del triplete booleano resuelto utilizando 200 terabytes de datos en mayo de 2016.​

Véase también

• Demostración en matemática
• Verificación de modelos
• Revisión de pruebas
• Cálculo simbólico
• Razonamiento automático
• Verificación formal
• Seventeen or Bust
• Metamath

Lecturas adicionales

• Lenat, D.B., (1976), AM: Un enfoque de inteligencia artificial para el descubrimiento en matemáticas como búsqueda heurística, Ph.D. Tesis, STAN-CS-76-570, y Heuristic Programming Project Report HPP-76-8, Stanford University, AI Lab., Stanford, CA.
• M. Nakao, M. Plum, Y. Watanabe (2019) Numerical Verification Methods and Computer-Assisted Proofs for Partial Differential Equations (Springer Series in Computational Mathematics).

Enlaces externos

• Oscar E. Lanford; Una prueba asistida por computadora de las conjeturas de Feigenbaum, "Bull. Amer. Math. Soc.", 1982
• Edmund Furse; ¿Por qué se ejecutó AM? fuera de vapor?
• Las pruebas numéricas hechas por la computadora podrían errar Archivado el 29 de junio de 2011 en Wayback Machine.
• «A Special Issue on Formal Proof». Notices of the American Mathematical Society. diciembre de 2008. 

• Datos: Q1150675