Cómo bien aceptados son pruebas donde las partes críticas dependen del software de las que nosotros no tenemos acceso a la fuente, e.g Mathematica, Maple?
Más generalmente, ¿cuánto podemos tomar en la fe con respecto a software. Tenemos que comprobar que el compilador para el Teorema de los Cuatro Colores?
Hace un par de años los Avisos de la Sociedad Matemática Americana publicó una serie de artículos sobre el estado del arte en el uso de equipo de prueba de los asistentes. Ellos son, al menos, la pena de succión.
"La Prueba Formal," por Thomas Hales
"La Prueba Formal - El Cuatro-Color Teorema," por Georges Gonthier
"La Prueba Formal de la Teoría y la Práctica," por John Harrison
"La Prueba Formal - introducción," por Freek Wiedijk
Tiendo a ser un tradicionalista cuando se trata de los métodos tradicionales frente a los métodos informáticos, pero yo lo encuentro argumentos como los siguientes convincente.
(Esto es de un comunicado de prensa de la AMS en su serie de artículos sobre la prueba formal.)
"Cuando los matemáticos demostrar teoremas de la forma tradicional, presentan el argumento en forma de narración. Ellos asumen que los resultados anteriores, se pasan por alto detalles que piensan otros expertos te entiendo, no tomar atajos para hacer la presentación menos tedioso, apelan a la intuición, etc. La corrección de los argumentos es determinado por el escrutinio de otros matemáticos, en conversaciones informales, en las conferencias, o en revistas. Es triste darse cuenta de que el medio por el cual los resultados matemáticos son verificados es esencialmente un proceso social y por lo tanto falible." [énfasis mío]
(Y esto es de Hales, del artículo).
"El equipo de código que implementa los axiomas y reglas de inferencia se conoce como el núcleo del sistema. Se tarda menos de 500 líneas de código informático para implementar el núcleo de HOL Luz."
La verificación de la corrección de un pequeño programa sería mucho más fácil a la hora de verificar la corrección de pruebas de muchos de los teoremas.
(También de Hales, del artículo).
"La experiencia de otros de nivel superior que el teorema demuestra sistemas ha sido que de tres a cinco errores han sido encontrados en cada sistema durante un período de 15 a 20 años de uso. Después de décadas de uso en muchos sistemas diferentes, a mi entender, sólo una prueba ha tenido que ser retirado como resultado de un error en un teorema-probando el sistema, y esto en un sistema que no me clasificación en el nivel superior... podemos afirmar con toda confianza que la tasa de error de nivel superior teoremas sistemas son órdenes de magnitud inferior a las tasas de error en los más prestigiosos matemáticos revistas." [énfasis mío]
Como una nota del lado, Hales, del papel también enumera varios de los principales teoremas (ya ha demostrado de la manera tradicional, por supuesto) que han sido ya demostrado por un equipo. Estos incluyen la reciprocidad cuadrática, el teorema de los números primos, los teoremas fundamentales del álgebra y el cálculo, el Jordán de la curva de teorema, y la Brouwer de punto fijo teorema.
Además de los Cuatro-Color Teorema de, al parecer, el Robbins conjetura se demostró por primera vez por un sistema automatizado teorema de armario.
Y, por supuesto, no hay en Wikipedia sobre asistida por ordenador, prueba.
Yo diría que para una mezcla de prueba del sistema. Equipo de pruebas debe ser más aceptado que son ahora, pero la tradición es lento para construir. Prefiero confiar en una prueba de que también ha sido evaluada por un equipo, además de las tradicionales de revisión por pares. Después de todo, sólo hay tanta cantidad de abstracción que un cerebro humano puede manejar, y a veces los pequeños detalles pueden cambiar todo. Como Alain Connes ponerlo en la Princeton Compañero, el paso más difícil en un trabajo matemático es la comprobación de errores.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
