L'idée n'est pas de remplacer le document décrivant la preuve par le code de la preuve mécanisée, mais de le complémenter. Aujourd'hui la preuve LaTeX a deux rôles, à la fois communiquer le résultat et s'assurer, du mieux possible, qu'il n'y a pas d'erreurs. C'est agréable quand on est un lecteur qui sait que la preuve a déjà été acceptée par la communauté et qui peut se concentrer sur la compréhension, mais pas pour :
les premiers rapporteurs/relecteurs, qui ont une lourde responsabilité vis-à-vis de la communauté et à qui la partie "re-vérifier les calculs et les arguments" peut demander énormément de travail (en plus du travail de compréhension d'ensemble, etc.)
l'auteur lui-même, qui n'a pas d'outils adapté pour, par exemple, savoir quelles parties du développement doivent être revues si il ou elle modifie une définition ou change une hypothèse
(Un exemple un peu extrême est la démonstration proposée de la conjecture ABC, qui a été proposée à la communauté en 2012 et dont on ne sait toujours pas si elle acceptée ou pas.)
Quand on utilise un assistant de preuve, les rapporteurs/reviewers doivent d'une part comprendre l'argument d'ensemble (comme avant) et les idées des preuves (comme avant). Pour savoir si les preuves sont correctes dans les détails, il suffit de lire les énoncés de la preuve mécanisée, et de se convaincre qu'ils correspondent effectivement aux énoncés de l'article informel (il peut bien sûr y avoir des erreurs à ce niveau-là); re-vérifier indépendamment la preuve mécanisée est ensuite "immédiat" (on fait tourner le programme vérificateur de preuve), et donne une confiance très forte dans la validité de la démonstration. Ça aide aussi beaucoup l'auteur en cas de modification de la preuve au cours de son écriture.
Une partie de ma communauté travaille déjà comme ça : dans certaines de nos conférences il y a un tiers (je dirais, à la louche) des soumissions qui viennent avec, en complément, une preuve mécanisée, et cela nous a permis d'attaquer des problèmes plus difficiles et de faire des raisonnements plus techniques avec confiance, et en gardant des temps de revue/relecture relativement courts (quelques mois).
(C'est aussi absolument nécessaire pour la preuve de programmes, où on écrit une preuve mathématique du fait qu'un programme correspond à une spécification. La nature très calculatoire de certaines parties de ces arguments fait qu'il est extrêmement pénible de relire les détails des preuves pour un humain, et que le risque d'erreur d'inattention augmente beaucoup.)
Un exemple typique est le livre "Homotopy Type Theory", qui a été entièrement formalisé avec un assistant de preuve (en Agda), en parallèle avec la rédaction du livre dans un style "informel" (non vérifié) mathématique classique.
[^] # Re: Math
Posté par gasche . En réponse au journal La recherche en langages de programmation au quotidien. Évalué à 5.
L'idée n'est pas de remplacer le document décrivant la preuve par le code de la preuve mécanisée, mais de le complémenter. Aujourd'hui la preuve LaTeX a deux rôles, à la fois communiquer le résultat et s'assurer, du mieux possible, qu'il n'y a pas d'erreurs. C'est agréable quand on est un lecteur qui sait que la preuve a déjà été acceptée par la communauté et qui peut se concentrer sur la compréhension, mais pas pour :
(Un exemple un peu extrême est la démonstration proposée de la conjecture ABC, qui a été proposée à la communauté en 2012 et dont on ne sait toujours pas si elle acceptée ou pas.)
Quand on utilise un assistant de preuve, les rapporteurs/reviewers doivent d'une part comprendre l'argument d'ensemble (comme avant) et les idées des preuves (comme avant). Pour savoir si les preuves sont correctes dans les détails, il suffit de lire les énoncés de la preuve mécanisée, et de se convaincre qu'ils correspondent effectivement aux énoncés de l'article informel (il peut bien sûr y avoir des erreurs à ce niveau-là); re-vérifier indépendamment la preuve mécanisée est ensuite "immédiat" (on fait tourner le programme vérificateur de preuve), et donne une confiance très forte dans la validité de la démonstration. Ça aide aussi beaucoup l'auteur en cas de modification de la preuve au cours de son écriture.
Une partie de ma communauté travaille déjà comme ça : dans certaines de nos conférences il y a un tiers (je dirais, à la louche) des soumissions qui viennent avec, en complément, une preuve mécanisée, et cela nous a permis d'attaquer des problèmes plus difficiles et de faire des raisonnements plus techniques avec confiance, et en gardant des temps de revue/relecture relativement courts (quelques mois).
(C'est aussi absolument nécessaire pour la preuve de programmes, où on écrit une preuve mathématique du fait qu'un programme correspond à une spécification. La nature très calculatoire de certaines parties de ces arguments fait qu'il est extrêmement pénible de relire les détails des preuves pour un humain, et que le risque d'erreur d'inattention augmente beaucoup.)
Un exemple typique est le livre "Homotopy Type Theory", qui a été entièrement formalisé avec un assistant de preuve (en Agda), en parallèle avec la rédaction du livre dans un style "informel" (non vérifié) mathématique classique.