En la filosofía de las matemáticas , una prueba no investigable es una prueba matemática que se considera inviable de verificar para un matemático humano y, por lo tanto, de validez controvertida . El término fue acuñado por Thomas Tymoczko en 1979 en crítica a la demostración asistida por computadora del teorema de los cuatro colores de Kenneth Appel y Wolfgang Haken , y desde entonces se ha aplicado a otros argumentos, principalmente aquellos con una división excesiva de casos y/o con porciones enviadas. mediante un programa informático difícil de verificar. La encuestabilidad 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 cumplió con el criterio de encuestabilidad al sustituir, argumentó, la deducción por experimento :
…si aceptamos el [Teorema de los cuatro colores] como teorema, nos comprometemos a cambiar el sentido de "teorema" o, más concretamente, a cambiar el sentido del concepto subyacente de "demostración".
…[el] uso de computadoras en matemáticas, como en el [Teorema de los cuatro colores], introduce experimentos empíricos en las matemáticas. Ya sea que decidamos considerar el [Teorema de los cuatro colores] como probado o no, debemos admitir que la prueba actual no es una prueba tradicional, ni una deducción a priori de un enunciado a partir de premisas. Es una prueba tradicional con una laguna 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 encuestabilidad, 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 desempeñar el papel de una observación más que de un argumento. [2] [3]
Esta distinción es importante porque significa que las pruebas no investigables exponen a las matemáticas a un potencial de error mucho mayor. Especialmente en el caso en el que la falta de capacidad de encuesta se debe al uso de un programa informático (que puede tener errores ), especialmente cuando ese programa no está publicado, la persuasión puede verse afectada como resultado. [3] Como escribió Tymoczko:
Supongamos que una supercomputadora se pusiera a trabajar en la consistencia de la aritmética de Peano y reportara una prueba de inconsistencia , una prueba que fuera tan larga y compleja que ningún matemático podría 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 de que las pruebas difíciles de estudiar no son necesariamente tan inválidas como las pruebas imposibles de estudiar.
Paul Teller afirmó que la encuestabilidad era una cuestión de grado y dependiente del lector, no algo que una prueba tenga o no tenga. Como las demostraciones no se rechazan cuando los estudiantes tienen problemas para comprenderlas, sostiene Teller, tampoco se deben rechazar (aunque pueden ser criticadas) simplemente porque a los matemáticos profesionales les resulte difícil seguir el argumento. [4] [3] (Teller no estuvo de acuerdo con la evaluación de Tymoczko de que "[El teorema de los cuatro colores] no ha sido verificado por los matemáticos, paso a paso, como lo han sido todas las demás pruebas. De hecho, no se puede verificar de esa manera". )
Un argumento similar es que la división de casos es un método de prueba aceptado, y la prueba de Appel-Haken es sólo un ejemplo extremo de división de casos. [2]
Por otro lado, el argumento de Tymoczko de que las pruebas deben ser al menos posibles de examinar y que es menos probable que los errores en las pruebas difíciles de examinar sean objeto de escrutinio no se cuestiona en general; en cambio, se han sugerido métodos para mejorar la encuestabilidad, especialmente de las pruebas asistidas por computadora. Una de las primeras sugerencias fue 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 presentar las partes dudosas de una prueba en un formalismo restringido y luego verificarlas con un verificador de pruebas que está disponible para su inspección. De hecho, así se ha verificado la prueba de Appel-Haken. [6]
No obstante, la verificación automatizada aún no ha tenido una adopción generalizada. [7]