Une preuve en math à la main peut être vérifiée, si longue soit-elle. C'est d'ailleurs ce qui s''est passé avec la preuve du théorème de Fermat. A partir du moment ou tu confies la vérification à la machine, il faut:
- avoir confiance dans le programme (ou le vérifier).
- avoir confiance dans les données qu'il reçoit (ou les vérifier).
La conjecture de Kepler montre qu'une certitude n'est pas si simple à obtenir. D'ailleurs un passage par un système de preuve à la coq semble en cours.
Pour les vérifications basées sur un système de preuve, il faut:
- vérifier que la modélisation correspond au problème.
- vérifier le moteur de preuve.
Il peut y avoir des choses intéressantes dans la modélisation, mais la preuve reste tributaire du moteur de preuve. Tant que la sortie reste trop complexe pour être transformée en preuve "humainement compréhensible".
Dans les deux cas ce ne sont pas des démonstrations du Livre. Les démonstrations du Livre elles sont directement belles.
[^] # Re: En souvenir de son infirmation de la conjecture des quatre couleurs.
Posté par fleny68 . En réponse au journal Martin Gardner (1914-2010). Évalué à 1.
- avoir confiance dans le programme (ou le vérifier).
- avoir confiance dans les données qu'il reçoit (ou les vérifier).
La conjecture de Kepler montre qu'une certitude n'est pas si simple à obtenir. D'ailleurs un passage par un système de preuve à la coq semble en cours.
Pour les vérifications basées sur un système de preuve, il faut:
- vérifier que la modélisation correspond au problème.
- vérifier le moteur de preuve.
Il peut y avoir des choses intéressantes dans la modélisation, mais la preuve reste tributaire du moteur de preuve. Tant que la sortie reste trop complexe pour être transformée en preuve "humainement compréhensible".
Dans les deux cas ce ne sont pas des démonstrations du Livre. Les démonstrations du Livre elles sont directement belles.