Un bogue de vérificateur de preuve a-t-il déjà invalidé une preuve majeure?

La plupart (tous?) Des assistants de preuve ont des bugs de solidité corrigés à l'occasion. Cependant, parmi ceux que j'ai vus, ces bogues sont généralement difficiles à trouver involontairement, et les résultats prouvés avant que le bogue ne soit corrigé se maintiennent généralement après la correction.

Trois questions, par ordre de force:

Une telle correction de bogue de solidité a-t-elle déjà causé l'échec d'une preuve majeure, sans modifier la preuve?
Si (1) est vrai, des modifications majeures ont-elles jamais été nécessaires pour corriger la preuve?
Si (2) est vrai, quelqu'un a-t-il prouvé un mauvais théorème majeur en raison d'un bug de solidité?

Je laisse la définition de «majeur» à d'autres.

proof-assistants soundness Geoffrey Irving
la source

Cela montre probablement mon ignorance, mais un théorème majeur a-t-il déjà été établi avec un assistant de preuve? Bien sûr, je connais le théorème des 4 couleurs et la conjecture de Kepler, mais je ne pense pas que les premières preuves là-bas utilisaient des assistants de preuve. Je suis curieux.

Sasho Nikolov

Je crois qu'aucun humain n'avait prouvé qu'un compilateur avait raison, et avait été correct à ce sujet, jusqu'à CompCert. Mais vous avez raison, cela rendrait (3) en particulier une question moins intéressante.

Geoffrey Irving

@SashoNikolov: ce n'est pas vraiment pertinent, car la plupart des preuves faites en pratique par des assistants de preuve ne concernent pas les mathématiques. Ils sont généralement sur les systèmes logiciels, ou sur les propriétés des systèmes formels, etc. (Il est seulement une question de temps où la grande majorité des preuves effectuées sur cette planète sont pas sur les mathématiques pures. Les robots arrivent.) Ce serait assez ennuyeux si, par exemple, quelqu'un a prouvé à l'aide d'un assistant de preuve qu'un système critique est sûr, puis il s'est avéré plus tard qu'il avait accidentellement utilisé une incohérence.

Andrej Bauer

Merci @AndrejBauer. Donc, «preuve majeure» et «théorème majeur» ne signifient pas ici majeur pour les mathématiciens de recherche, mais des preuves de l'exactitude de systèmes critiques importants?

Sasho Nikolov

Je pense que toute preuve jugée importante par suffisamment de personnes (mathématiciens, experts en sécurité, ingénieurs logiciels) compterait. Je crains que nous n'allons pas le découvrir parce que si quelqu'un a trébuché sur ce problème, il y a de fortes chances qu'il le répare tranquillement.

Andrej Bauer

Réponses:

À ma connaissance, aucune preuve vérifiée par machine d'un développement mathématique complexe n'a jamais été rétractée.

Comme Andrej souligne cependant, il arrive parfois que les bugs briser la solidité ne surgissent dans ces systèmes (mais généralement pas en silence , comme Andrej suggère), et le correctif à ce bogue implique des changements aux preuves existantes, ou, plus probablement, de la bibliothèque standard du système de preuve impliqué.

Quelques exemples de telles preuves de rupture de bibliothèque dans Coq:

https://coq.inria.fr/bugs/show_bug.cgi?id=4294

https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html

Il est difficile de dire si les preuves établies dépendent de l'incohérence, car après le correctif, elles nécessitaient des ajustements mineurs pour être acceptés par le vérificateur. Mais cela se produit à chaque mise à jour non triviale!

Mon opinion personnelle est qu'il est peu probable que de telles erreurs se produisent, car l' épreuve papier doit être bien polie avant même que la formalisation de la machine ne puisse être tentée.

Les incohérences dans les cadres de preuve nécessitent généralement l'utilisation intensive de combinaisons étranges de caractéristiques ésotériques, et surviennent donc très rarement "par accident".

cody
la source

Je faisais référence à des personnes résolvant les problèmes dans leurs scripts de preuve en silence , ou même à leur insu, comme Geoffrey l'a souligné, en réaction à des bogues dans les assistants de preuve. Bien sûr, les incohérences dans les assistants de preuve sont toujours reçues avec un niveau d'excitation incroyable. Les mathématiciens devraient avoir une incohérence dans les mathématiques, ce qui donnerait quelques mois intéressants.

Andrej Bauer

Qu'est-ce que c'est que les gens qui me lancent des liens Wikipedia? @RickyDemer, voulez-vous bien vouloir expliquer votre point. J'ai entendu parler du paradoxe de Russell, vous savez. C'était il y a plus de 100 ans, et cela a conduit à d'excellentes mathématiques. Je propose que nous soyons mûrs pour un autre.

Andrej Bauer

J'accepterai cette réponse pour l'instant, mais bien sûr je ne l'accepterai pas si quelqu'un répond dans l'autre sens! (Divulgation complète: c'était la réponse que j'espérais.)

Geoffrey Irving

@GeoffreyIrving La réponse est quelque peu insatisfaisante, car il m'est difficile de prouver un manque de rétractations! La réponse est donc quelque peu nécessairement basée sur mon manque de connaissances, bien qu'il y ait eu si peu de formalisations de machines à très grande échelle que je suis au moins un peu confiant dans ma réponse. J'ai également entendu dire que certaines formalisations importantes dans la méthode B se sont avérées avoir des hypothèses incohérentes (vous devez ajouter de nombreux axiomes pour les déclarations non triviales, et les collections d'axiomes prises ensemble se sont révélées être par la suite ...

cody

... inconsistant). Malheureusement, je n'arrive pas à trouver de référence pour cela, donc je ne l'ai pas inclus dans ma réponse. La formalisation concernait également un grand programme et non des mathématiques pures.

cody