Des mathématiciens se lancent dans une preuve informatique du « dernier théorème de Fermat », une énigme vieille de 350 ans
(dongascience.com)Le dernier théorème de Fermat va être démontré à nouveau dans un langage informatique
- Le professeur Kevin Buzzard de l'Imperial College London prévoit de rédiger à partir d'octobre 2024 une preuve formelle du dernier théorème de Fermat (FLT) avec le démonstrateur de théorèmes Lean.
- Le Conseil de recherche en ingénierie et sciences physiques [EPSRC] du Royaume-Uni a décidé d'accorder à partir de ce mois-là un financement de recherche au professeur Buzzard pendant cinq ans.
- Un document de planification du projet, créé à l'aide de Lean blueprints, un plugin plasTeX, devrait être publié vers la fin avril 2024.
Le dernier théorème de Fermat n'a-t-il pas déjà été démontré ?
Si, il l'a déjà été. Le mathématicien britannique Andrew Wiles a rendu publique sa démonstration en 1994, et celle-ci a été officiellement publiée en 1995. En revanche, il n'existe pas encore de preuve formelle rédigée dans le langage d'un démonstrateur de théorèmes interactif [ITP].
Démonstrateur de théorèmes interactif ? Preuve formelle ? Qu'est-ce que c'est ?
- Démonstrateur de théorèmes interactif [ITP] : programme informatique qui aide les humains à écrire des preuves formelles. On l'appelle aussi assistant de preuve[proof assistant].
- Preuve formelle : preuve qu'un programme informatique appelé vérificateur de preuves[proof verifier] peut vérifier. Un assistant de preuve fait généralement aussi office de vérificateur de preuves.
Les démonstrateurs de théorèmes sont-ils une IA ?
Les neural theorem provers [NTP] peuvent être considérés comme tels, mais de nombreux démonstrateurs de théorèmes interactifs, dont Lean, ne sont pas des programmes fondés sur l'apprentissage automatique.
Présente-moi le démonstrateur de théorèmes Lean.
- Démonstrateur de théorèmes interactif et langage de programmation purement fonctionnel.
- Repose sur la théorie des types dépendants.
- Il dispose de fonctionnalités telles que les classes de types, une syntaxe extensible, les macros et la métaprogrammation.
- Par rapport aux autres assistants de preuve, Lean compte parmi ses utilisateurs un nombre particulièrement élevé de mathématiciens (notamment hors fondements des mathématiques).
Pourquoi vouloir écrire une preuve formelle du dernier théorème de Fermat ?
Pour citer un post publié sur X par le professeur Kevin Buzzard : « Il s'agit d'amener l'ordinateur à comprendre la théorie moderne des nombres, afin qu'il puisse à terme aider les théoriciens des nombres. »
Liens
- Message publié par le professeur Kevin Buzzard sur le chat Zulip de Lean le 3 octobre 2023 : https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/…
- Bibliothèque mathématique de Lean : https://github.com/leanprover-community/mathlib4
- Article de New Scientist : https://institutions.newscientist.com/article/…
- Article de Popular Mechanics : https://popularmechanics.com/science/math/…
1 commentaires
Je vous soutiens. Pour celles et ceux qui s’intéressent aux preuves formelles, je recommande aussi d’écouter le cours Machine Assisted Proofs du professeur Terrence Tao (https://www.youtube.com/watch?v=AayZuuDDKP0).