En la filosofía de las matemáticas , una prueba no verificable es una prueba matemática que se considera inviable para que un matemático humano la verifique y, por lo tanto, de validez controvertida . El término fue acuñado por Thomas Tymoczko en 1979 como crítica a la prueba asistida por computadora de Kenneth Appel y Wolfgang Haken del teorema de los cuatro colores , y desde entonces se ha aplicado a otros argumentos, principalmente aquellos con división excesiva de casos y/o con porciones distribuidas por un programa informático difícil de verificar. La verificabilidad sigue siendo una consideración importante en las matemáticas computacionales .
Tymoczko argumentó que tres criterios determinan si un argumento es una prueba matemática:
En opinión de Tymoczko, la prueba de Appel-Haken no cumplía el criterio de observabilidad porque, según él, sustituye la deducción por el experimento :
…si aceptamos el [Teorema de los Cuatro Colores] como un teorema, nos comprometemos a cambiar el sentido de "teorema", o, más concretamente, a cambiar el sentido del concepto subyacente de "prueba".
…[el] uso de computadoras en matemáticas, como en el [Teorema de los Cuatro Colores], introduce experimentos empíricos en las matemáticas. Tanto si optamos por considerar el [Teorema de los Cuatro Colores] como demostrado, debemos admitir que la prueba actual no es una prueba tradicional, ni una deducción a priori de una afirmación a partir de premisas. Es una prueba tradicional con una laguna, o vacío, que se llena con los resultados de un experimento bien pensado.— Thomas Tymoczko, "El problema de los cuatro colores y su significado filosófico" [1]
Sin capacidad de análisis, una prueba puede cumplir su primer propósito de convencer al lector de su resultado y, sin embargo, fallar en su segundo propósito de ilustrar al lector sobre por qué ese resultado es verdadero; puede cumplir el papel de una observación más que de un argumento. [2] [3]
Esta distinción es importante porque significa que las pruebas que no se pueden estudiar exponen a las matemáticas a un potencial de error mucho mayor. Especialmente en el caso en que la no posibilidad de estudiar se debe al uso de un programa informático (que puede tener errores ), sobre todo cuando ese programa no está publicado, la convicción puede verse afectada como resultado. [3] Como escribió Tymoczko:
Supongamos que se pusiera a trabajar a una supercomputadora sobre la consistencia de la aritmética de Peano y que esta diera una prueba de inconsistencia , una prueba que fuera tan larga y compleja que ningún matemático pudiera entenderla más allá de los términos más generales. ¿Podríamos tener suficiente fe en las computadoras para aceptar este resultado, o diríamos que la evidencia empírica de su confiabilidad no es suficiente?
— Thomas Tymoczko, "El problema de los cuatro colores y su significado filosófico" [1]
Sin embargo, la opinión de Tymoczko es cuestionada por argumentos que sostienen que las pruebas difíciles de examinar no son necesariamente tan inválidas como las pruebas imposibles de examinar.
Paul Teller afirmó que la posibilidad de ser examinada era una cuestión de grado y dependiente del lector, no algo que una prueba tenga o no tenga. Teller sostiene que, como las pruebas no se rechazan cuando los estudiantes tienen problemas para comprenderlas, tampoco se deberían rechazar (aunque se las pueda criticar) simplemente porque a los matemáticos profesionales les resulte difícil seguir el argumento. [4] [3] (Teller no estaba de acuerdo con la afirmación de Tymoczko de que "[El teorema de los cuatro colores] no ha sido comprobado por los matemáticos, paso a paso, como se ha comprobado todas las demás pruebas. De hecho, no se puede comprobar de esa manera").
Un argumento similar es que la división de casos es un método de prueba aceptado y que la prueba de Appel-Haken es sólo un ejemplo extremo de división de casos. [2]
Por otra parte, el argumento de Tymoczko de que las pruebas deben ser al menos posibles de examinar y que los errores en las pruebas difíciles de examinar tienen menos probabilidades de ser examinados no suele ser cuestionado; en cambio, se han sugerido métodos para mejorar la examinabilidad, especialmente de las pruebas asistidas por computadora. Entre las primeras sugerencias estaba la de la paralelización: la tarea de verificación podría dividirse entre muchos lectores, cada uno de los cuales podría examinar una parte de la prueba. [5] Pero la práctica moderna, como la hizo famosa Flyspeck , es convertir las partes dudosas de una prueba en un formalismo restringido y luego verificarlas con un verificador de pruebas que está disponible para su examen. De hecho, la prueba de Appel-Haken ha sido verificada de esta manera. [6]
Sin embargo, la verificación automatizada aún no ha sido ampliamente adoptada. [7]