On sent l'auteur qui souffle
Par David Monniaux le samedi, février 18 2012, 13:37 - Enseignement - Lien permanent
On pourrait croire que les mathématiques sont le domaine de la rigueur absolue, où tout doit être explicité en détail. En réalité, les preuves mathématiques courantes sont pleines d'appels à l'intelligence du lecteur, de non-dits, d'omissions de détails ou de calculs fastidieux ; sinon, d'ailleurs, elles seraient vite illisibles, ou extrèmement fastidieuses...
Il y a toutefois des sujets que l'on aime détailler.. et ceux où l'on souffle, on réfléchit à un moyen simple et bref d'y arriver, et finalement on renonce et on dit que c'est un résultat classique mais pénible (on sent d'ailleurs quasiment chez certains auteurs l'essoufflement associé). Parmi ces derniers, je relève :
- L'écriture d'une machine de Turing universelle.
- L'écriture de la preuve formelle dans l'arithmétique de Robinson du premier théorème d'incomplétude de Gödel, notamment de l'adéquation de la numérotation de Gödel utilisée par rapport aux conditions de Hilbert-Bernays, pour obtenir la preuve du deuxième théorème d'incomplétude.
Et vous ?
Commentaires
Il est utile de lire "preuves et réfutations" de Lakatos pour revenir de la croyance en la rigueur absolue des mathématiques.
@kuk: Il suffit d'être soi-même mathématicien ou apparenté.
pendant mes études, j'ai toujours été "horrifié" du peu de rigueur dans la facon d'utiliser les math dans les cours de physique que je suivais.
Mais on ne pouvait pas garder une rigueur mathématique aussi formel à moins de faire un cours de math dans le cours de physique.
Ca marchait a l'à peu près.
La rigueur demande d'être exhaustif, non ?
@David Monniaux : A partir de quel stade d'étude est-on mathématicien ou apparenté ?
@kuk: Si on a un travail consistant, du moins en partie, à prouver des théorèmes et à en rédiger les preuves. :-)
Belle réponse. Mais alors ma proposition est peut être plus facile à mettre en œuvre :-)
Sinon, le théorème des 4 couleurs ne doit pas être très marrant à démontrer.
Bien souvent, on peut découper un théorème en sous-propositions de longueurs plus abordables. Le théorème ne se résume alors qu'à quelques lignes, indiquant cet enchaînement. Le cas que vous évoquez doit donc concerner des théorèmes plus ou moins "insécables" et longs...
@kuk: On parle souvent de la longueur des preuves, mais, comme vous le soulignes, une preuve longue peut être assez facile si on peut la découper en lemmes ; c'est ce qui se découpe mal qui est dur. Juris Hartmanis et d'autres ont introduit une notion de « largeur » de preuve, qui, en termes intuitifs, correspond à la quantité de lemmes et hypothèses que l'on doit simultanément avoir au pire endroit de la preuve (bien sûr, la définition formelle est plus technique).
C'est pas fondamentalement different de l'ecriture d'un programme. Des qu'on implemente un algo un peu complexe, ca devient la-aussi delicat a decouper proprement.
Deux differences peut-etre:
- le fomalisme va plus loin. Ca marche ou ca casse.
- on peut experimenter plus librement, faire facilement de petites transformations ET verifier mecaniquement que ca marche toujours.
La 2e difference est toute con, mais elle permet de souffler moins souvent: on peut opposer de belles techniques d'abstraction a l'ecriture d'un code complique, et avoir un validateur automatique.
Comme a peu pres personne n'utilise le meme type de validateur pour des preuves mathematiques (qui utilise coq pour autre chose que des trivialites ? quel pourcentage de mathematicien maitrise des outils de preuve formelle), obligatoirement, l'ecriture de preuve mathematique, c'est plus de l'art, et moins de la
sciencetechnologie appliquee. ;)Bonjour.
En même temps, la discussion entre les démonstrateurs automatisés et les preuves papier/crayon montrent exactement la source du problème soulevé ici. Lorsqu'on prouve un théorème avec une machine, on ne peut pas vraiment "cacher" les détails : tout doit être prouvé, quitte à ce que ce soit de manière assistée (mais les parties difficiles sont rarement assistables, justement). Lorsqu'on prouve au papier/crayon, on fait justement preuve de discernement : on indique les étapes à prouver, et quelqu'un qui a plus ou moins la même expertise du domaine peut en retrouver les étapes et les valider lui-même.
Il y a donc deux travers évidents. Si on devait tout détailler en maths, il faudrait des articles de la longueur d'une thèse, voire plus... Et c'est justement un critère d'évaluation de mathématiciens : quelles étapes sont nécessairement détaillées pour comprendre la preuve générale ? Tout est affaire d'un peu, mais pas trop... De l'autre côté du spectre, on connaît le problème : ces preuves dont on dit trop vite qu'on l'a démontré, mais qui reste des années, voire des siècles, à recevoir une preuve digne de ce nom...
Et puis, comme à l'âge d'or du model-checking, on peut poser la question théorique de la validation des validateurs (mathématiques). C'est d'ailleurs vrai pour n'importe quel outil informatique dont la vocation se veut formelle : comment prouver qu'il fait bien ce qu'il fait (les intérpréteurs abstraits aussi, d'ailleurs, non ?) Les gens de PVS disaient à l'époque : tellement de gens utilisent PVS que si un bug subtile existe, les utilisateurs l'auraient vu... C'est vrai pour les preuves de complexité commune, mais il existe toujours des bugs, pas toujours dûs à la théorie elle-même, mais parfois parce qu'une preuve requiert de sortir les tréfonds de l'outil que personne n'a jamais vraiment expérimenté avant...
Il y a plein de preuves comme ça, qui sont juste données à coup de "sketch proof". J'ai lu dernièrement plusieurs preuves sur la terminaison et la confluence de systèmes de transformations sur des graphes, et j'ai un doute raisonnable... Mais l'auteur clame que la preuve est juste... parce que l'outil implémente les algos et qu'il termine et conflue... Ca laisse songeur...
PS: @Kuk Merci pour la suggestion de lecture!!!
@Potatoes: Je suis assez d'accord avec vos remarques, mais juste un point: effectivement, avec PVS ou ACL2, s'il y a un bug dans les procédures de décision etc. de l'outil, vous pouvez prouver des faussetés; avec Coq, les preuves sont in fine exprimées comme des λ-termes, et une procédure relativement simple vérifie qu'ils sont bien typés, ce qui limite les possibilités de bug.
Qu'en est-il donc des interpréteurs abstraits, alors ? Est-ce que la même question de la "vérification du vérificateur" se pose dans les mêmes termes ou bien est-ce différent ?
Je ne connais pas assez la mécanique derrière leur(s) implémentation(s) : Astrée est trop gros pour qu'on puisse en faire une étude dans ce sens, et les rares tentatives académiques font des outils qui n'ont pas encore la même mâturité que les theorem-provers ou les model-checkers...
Une idée ? Ca m'intéresse... Y a-t-il des gens qui reportent leur expérience de l'implémentation d'un tel outil (pas Astrée, hein... lol)
Pour Coq en effet, si je me souviens bien, le langage est bootstrapé sur un noyau qui implémente un coeur de calcul minimum dont l'implémentation remonte déjà à longtemps. Au final, on sait plus ou moins que ce coeur fonctionne bien, et il suffit donc de faire évoluer le langage (rajouter des librairies, etc.) en les codant en Coq lui-même... Tant qu'on n'a pas besoin de faire évoluer la théorie (ce qui semble ne pas devoir arriver avant longtemps...), on est bon :-)
@Potatoes: Pour les interpréteurs abstraits en Coq, voir le projet VERASCO et les travaux de David Pichardie.
> Tant qu'on n'a pas besoin de faire évoluer la théorie
> (ce qui semble ne pas devoir arriver avant longtemps...),
Ouais, on va dire ça, hein.
These are not the droid you are looking for.
@Arnaud Spiwack @Potatoes: Ouais, par exemple, si on veut changer les règles pour qu'elles intègrent la proof-irrelevance (y compris sous une forme faible, par exemple l'axiome K de Streicher), ou si on intègre des tableaux natifs, etc. :-)
Ouais, je ne me sens pas visé du tout.
L'un dans l'autre, il y plein de changement du noyau qui sont pending et pour lesquelles ont se tate pour l'intégration (certains sont moins triviaux que d'autres).
Par ailleurs on trouve régulièrement des bugs qui permettent de prouver le faux. Donc la situation est plus subtile qu'il n'y paraît. Néanmoins, le fait que personne n'ait utilisé ce genre de bug sans s'en rendre compte rend plutôt optimiste quant à la validité des démonstrations Coq (largement plus souvent que les preuves papier, en tout cas).
Et puis, le noyau Coq est partiellement prouvé en Coq (par Bruno Barras). Et ça aide pas mal en fait.