N.B. : Je ne parle que des assistants à la preuve (surtout ceux basés sur le principe de de Bruijn pour les connaisseurs).
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).
J'ai plus confiance en un programme simple (< 10 kloc) et unique vérifié par des dizaines d'experts qu'en un humain, fut-il mathématicien. D'autant plus que toutes les preuves ne bénéficient pas de l'attention soutenue d'un comité de génies ; passons aimablement sur les lemmes « triviaux donc laissés à la charge du lecteur », facilité dont un ordinateur ne se satisfera que très partiellement. Est-ce grave ? Franchement, je ne le pense pas. Je m'élève juste contre des affirmations à l'emporte-pièce qui mélangent un peu preuve par ordinateur et cuisine numérique tendance empirisme-vaudou.
[^] # Re: En souvenir de son infirmation de la conjecture des quatre couleurs.
Posté par auve . En réponse au journal Martin Gardner (1914-2010). Évalué à 3.
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).
J'ai plus confiance en un programme simple (< 10 kloc) et unique vérifié par des dizaines d'experts qu'en un humain, fut-il mathématicien. D'autant plus que toutes les preuves ne bénéficient pas de l'attention soutenue d'un comité de génies ; passons aimablement sur les lemmes « triviaux donc laissés à la charge du lecteur », facilité dont un ordinateur ne se satisfera que très partiellement. Est-ce grave ? Franchement, je ne le pense pas. Je m'élève juste contre des affirmations à l'emporte-pièce qui mélangent un peu preuve par ordinateur et cuisine numérique tendance empirisme-vaudou.
Un peu de lecture : http://coq.inria.fr/faq?som=2#htoc7
- avoir confiance dans les données qu'il reçoit (ou les vérifier).
Quelles données ? Du moment que le théorème est bien écrit, tu n'as justement pas à vérifier la preuve, et c'est tout le principe.