La mayoría de los asistentes de prueba (¿todos?) Tienen errores de solidez corregidos ocasionalmente. Sin embargo, de los que he visto, estos errores suelen ser difíciles de encontrar involuntariamente, y los resultados probados antes de que el error se solucione generalmente se mantienen después de la corrección.
Tres preguntas, en orden de fortaleza:
- ¿Alguna corrección de errores de sonido ha causado alguna falla importante en una prueba, sin modificar la prueba?
- Si (1) es verdadero, ¿alguna vez se requirieron modificaciones importantes para arreglar la prueba?
- Si (2) es cierto, ¿alguien ha demostrado un teorema mayor incorrecto debido a un error de solidez?
Dejaré la definición de "mayor" a otros.
proof-assistants
soundness
Geoffrey Irving
fuente
fuente
Respuestas:
Que yo sepa, ninguna prueba comprobada por máquina de un complejo desarrollo matemático ha sido retractada.
Como Andrej señala, sin embargo, que en ocasiones sucede que los errores de solidez sin precedentes no surgen en estos sistemas (aunque por lo general no en silencio , como sugiere Andrej), y la solución a ese error implica algunos cambios en las pruebas existentes, o, más probablemente, de la biblioteca estándar del sistema de prueba involucrado.
Algunos ejemplos de tales pruebas de ruptura de bibliotecas en Coq:
https://coq.inria.fr/bugs/show_bug.cgi?id=4294
https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html
Es difícil decir si las pruebas establecidas dependían de la inconsistencia, ya que después de la corrección, requirieron pequeños ajustes para ser aceptados por el verificador de pruebas. ¡Pero esto sucede en cada actualización no trivial!
Mi opinión personal es que es poco probable que ocurran tales errores, ya que la prueba en papel debe pulirse bien antes de que se pueda intentar la formalización de la máquina.
Las inconsistencias en los marcos de prueba generalmente requieren el uso intensivo de combinaciones extrañas de características esotéricas, y muy raramente surgen "por accidente".
fuente