prueba asistida por ordenador

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 . 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 ) no comparten las implicaciones controvertidas de las pruebas asistidas por ordenador mediante agotamiento.