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.
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.
Más precisamente, si se reduce el cálculo a una secuencia de operaciones elementales, como (+, -, *, /).
Sin embargo, puede construirse un intervalo proporcionado por límites superiores e inferiores sobre el resultado de una operación elemental.
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.
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.
