Prueba asistida por computadora

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

Hasta la fecha, la mayoría de las demostraciones asistidas por ordenador han consistido en 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 demostrar que el resultado de estos cálculos implica el teorema en cuestión. En 1976, el teorema de los cuatro colores fue el primer teorema importante que se verificó mediante un programa informático .

En el campo de la investigación en inteligencia artificial , también se han realizado intentos para crear demostraciones nuevas, explícitas y más concisas de teoremas matemáticos, partiendo de técnicas de razonamiento automatizado como la búsqueda heurística . Estos demostradores automáticos de teoremas han probado varios resultados nuevos y encontrado nuevas demostraciones para teoremas conocidos. Además, los asistentes interactivos de demostración permiten a los matemáticos desarrollar demostraciones legibles por humanos que, sin embargo, se verifican formalmente. Dado que estas demostraciones suelen ser revisables por humanos (aunque con dificultad, como en el caso de la demostración de la conjetura de Robbins ), no presentan las implicaciones controvertidas de las demostraciones por agotamiento asistidas por computadora.

Un método para utilizar ordenadores en demostraciones matemáticas es mediante la llamada computación numérica validada o computación numérica rigurosa. Esto significa calcular numéricamente, pero con rigor matemático. Se utiliza aritmética de conjuntos y el principio de inclusión para asegurar que la salida de un programa numérico, también de conjuntos, englobe la solución del problema matemático original. Esto se logra controlando, englobando y propagando los errores de redondeo y truncamiento, utilizando, por ejemplo, aritmética de intervalos . Más precisamente, se reduce el cálculo a una secuencia de operaciones elementales, por ejemplo,${\displaystyle (+,-,\times ,/)}$En una computadora, el resultado de cada operación elemental se redondea según la precisión de la computadora. Sin embargo, se puede construir un intervalo a partir de los límites superior e inferior del resultado de una operación elemental. Luego, se procede reemplazando los números con intervalos y realizando operaciones elementales entre dichos intervalos de números representables.

Las demostraciones asistidas por ordenador son objeto de cierta controversia en el mundo matemático, siendo Thomas Tymoczko el primero en articular objeciones. Quienes se adhieren a los argumentos de Tymoczko creen que las extensas demostraciones asistidas por ordenador no son, en cierto sentido, demostraciones matemáticas «reales» porque implican tantos pasos lógicos que no son prácticamente verificables por seres humanos, y que, en efecto, se les pide a los matemáticos que reemplacen la deducción lógica a partir de axiomas supuestos con 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 el hardware. ^{[ 1 ]}

Otros matemáticos creen que las demostraciones extensas asistidas por computadora deberían considerarse cálculos , en lugar de demostraciones : el algoritmo de demostración en sí mismo debería ser validado, de modo que su uso pueda considerarse una mera "verificación". Los argumentos que sostienen 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 informático (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 diferentes equipos informáticos.

Otra forma posible de verificar las demostraciones asistidas por computadora consiste en generar sus pasos de razonamiento en un formato legible por máquina y, posteriormente, utilizar un programa de verificación para demostrar su corrección. Dado que validar una demostración es mucho más sencillo que encontrarla, el programa de verificación es más simple que el programa auxiliar original y, por consiguiente, resulta más fácil confiar en su corrección. Sin embargo, este enfoque de utilizar un programa informático para demostrar la corrección del resultado de otro programa no convence a los escépticos de las demostraciones computacionales, quienes lo consideran una capa adicional de complejidad sin abordar la necesidad percibida de comprensión humana.

Otro argumento en contra de las demostraciones asistidas por ordenador es que carecen de elegancia matemática , es decir, que no aportan ideas ni conceptos nuevos y útiles. De hecho, este argumento podría aplicarse a 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 adquiere mayor importancia que la aplicación de la razón pura en el ámbito de los conceptos matemáticos abstractos. Esto se relaciona directamente con el debate matemático sobre si las matemáticas se basan en ideas o son simplemente un ejercicio de manipulación de símbolos formales. También plantea la cuestión de si, según la visión platónica , todos los objetos matemáticos posibles "ya existen" en cierto sentido, si las matemáticas asistidas por ordenador constituyen una ciencia observacional como la astronomía, en lugar de una experimental como la física o la química. Esta controversia en matemáticas surge al mismo tiempo que se plantean en la comunidad física preguntas 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á abordando este debate de frente, centrándose en los experimentos numéricos como su principal herramienta para la exploración matemática.

La inclusión en esta lista no implica la existencia de una prueba formal verificada por ordenador, sino más bien que se ha utilizado algún programa informático. Consulte los artículos principales para obtener más detalles.

• Lenat, DB (1976). AM: Un enfoque de inteligencia artificial para el descubrimiento en matemáticas como búsqueda heurística (PDF) (PhD). AI Lab., Universidad de Stanford. STAN-CS-76-570, Informe del proyecto de programación heurística HPP-76-8.
• Meyer, KR; Schmidt, DS, eds. (2012). Demostraciones asistidas por ordenador en análisis . Volúmenes 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 demostraciones asistidas por computadora para ecuaciones diferenciales parciales . Springer Series in Computational Mathematics. Springer. ISBN 9789811376696.

• Lanford, Oscar E. (1982). "Una demostración 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é se agotó el impulso de AM? (Informe técnico). Departamento de Estudios Informáticos, Universidad de Glamorgan. CS-90-4. Archivado del original el 17 de julio de 2012. Consultado el 6 de septiembre de 2016 .{{cite tech report}}: CS1 maint: bot: estado de la URL original desconocido ( enlace )
• Begley, S. (16 de abril de 2018). "Las demostraciones numéricas realizadas por computadora podrían contener errores" . Pittsburgh Post-Gazette . Archivado del original el 16 de abril de 2018.
• "Número especial sobre demostración formal" . Notices of the American Mathematical Society . Diciembre de 2008.