En mai 2026, lorsqu'on évoque la formalisation mathématique assistée par ordinateur, la question revient systématiquement : « Pourquoi ne pas simplement utiliser Lean ? » Cette interrogation révèle une tendance préoccupante dans le monde de l'intelligence artificielle et de la logique computationnelle : le conformisme technologique qui efface près de 60 ans d'innovations.
Lean est effectivement un langage remarquable, doté d'outils performants, d'une bibliothèque conséquente et d'une communauté enthousiaste qui accomplit des prouesses impressionnantes. Mais réduire l'histoire de la formalisation mathématique à ce seul outil revient à ignorer des décennies de recherches fondamentales qui ont façonné le paysage actuel.
Cette approche exclusive rappelle les débats sur le nationalisme technologique qui opposent collaboration mondiale et solutions propriétaires. Explorons donc l'histoire méconnue des assistants de preuve et pourquoi la diversité technologique demeure essentielle.
AUTOMATH : le pionnier oublié de 1968
Contrairement aux affirmations fréquentes selon lesquelles « Lean a rendu possible la formalisation mathématique », cette discipline remonte à 1968 avec AUTOMATH, développé par NG de Bruijn. Ce système contenait déjà la plupart des ingrédients nécessaires à la formalisation rigoureuse.
En 1977, Jutting utilisa AUTOMATH pour formaliser les Fondations de l'Analyse de Landau, couvrant la construction des nombres complexes à partir de la logique pure. Il travailla avec des classes d'équivalence et des ensembles de nombres rationnels, prouvant formellement la complétude de Dedekind de la droite réelle.
Cet accomplissement ne fut égalé que 20 ans plus tard, malgré les progrès considérables de la puissance de calcul. Dans les années 90, les nombres réels furent à nouveau formalisés par John Harrison avec HOL Light et Jacques Fleuriot avec Isabelle/HOL.
Les forces méconnues d'AUTOMATH
Presque tout ce qui a été formalisé aujourd'hui dans n'importe quel système aurait pu l'être dans AUTOMATH. Ses principaux défauts concernaient sa notation particulièrement difficile et son absence totale d'automatisation, rendant les preuves longues et illisibles.
Paradoxalement, pour le raisonnement sur les classes d'équivalence, AUTOMATH reste probablement supérieur à Rocq (anciennement Coq). Tandis que les utilisateurs de ce dernier se plaignent de « l'enfer des setoïdes », Jutting décrivit posément dans sa thèse sa formalisation des classes d'équivalence, qu'il considérait comme l'approche correcte.
Boyer-Moore et la logique computationnelle
D'un horizon complètement différent émergea le travail de Robert Boyer et J Moore. Annoncé en 1973 avec le titre « Prouver des théorèmes sur les fonctions LISP », leur objectif visait la vérification de code plutôt que les mathématiques.
Leur « logique computationnelle » présente des limitations évidentes pour les mathématiques générales, mais cela n'a pas empêché son utilisation pour formaliser divers résultats profonds : le théorème d'incomplétude de Gödel, la réciprocité quadratique, ou le théorème de Banach-Tarski.
L'incarnation actuelle, ACL2, s'applique principalement à la vérification matérielle. Cette approche différente démontre qu'on peut aller loin en empruntant des chemins non conventionnels, un principe qui s'applique également aux modèles d'IA pour la recherche scientifique.
L'héritage du LCF d'Édimbourg
Le LCF d'Édimbourg se concentrait étroitement sur la théorie des langages de programmation, mais son idée d'utiliser un langage de programmation fonctionnel comme métalangage (d'où ML) d'un assistant de preuve eut un impact considérable.
La diversification : HOL, Coq et Isabelle
Des groupes à Cambridge, à l'INRIA, à Cornell et ailleurs construisirent des outils utilisant ML, incluant les premières versions de HOL, Coq (maintenant Rocq) et Nuprl. Le groupe HOL se concentrait sur la vérification matérielle, mais la nécessité de vérifier les unités de calcul en virgule flottante entraîna un besoin d'analyse réelle.
Rapidement, John Harrison prouva des résultats mathématiques sérieux, comme le théorème des nombres premiers via la formule intégrale de Cauchy. Il se fixa comme tâche de vérifier autant de théorèmes célèbres que possible, et HOL Light domine souvent ce classement.
| Système | Année de création | Spécialité initiale | Évolution majeure |
|---|---|---|---|
| AUTOMATH | 1968 | Formalisation pure | Classes d'équivalence |
| Boyer-Moore/ACL2 | 1973 | Vérification de code | Vérification matérielle |
| HOL Light | Années 80 | Vérification matérielle | Analyse réelle avancée |
| Isabelle | Années 80 | Logique générale | Automatisation poussée |
| Rocq (Coq) | Années 80 | Preuves constructives | Bibliothèques mathématiques |
| Lean | Années 2010 | Mathématiques modernes | Adoption massive |
Les grandes formalisations avant Lean
En 2014, ces systèmes avaient déjà formalisé une série de résultats avancés remarquables :
- Le théorème des quatre couleurs
- Le théorème de l'ordre impair
- La cohérence relative de l'axiome du choix
- Le second théorème d'incomplétude de Gödel
- La preuve de Tom Hales de la conjecture de Kepler
Ces théorèmes possédaient généralement des preuves longues et complexes. Leurs formalisations, travaux d'envergure, furent essentielles pour réduire les doutes résiduels. Pourtant, peu de mathématiciens furent impressionnés, à l'exception notable de Dana Scott et Ken Kunen, tous deux théoriciens des ensembles.
Les mathématiciens notaient que ces preuves n'impliquaient pas les constructions sophistiquées caractéristiques des mathématiques contemporaines : schémas de Grothendieck, espaces perfectoïdes, etc. Cette lacune allait motiver l'émergence de Lean.
L'émergence de la communauté Lean
Tom Hales eut l'idée de constituer une bibliothèque de définitions mathématiques sophistiquées – uniquement les définitions, sans les preuves – et choisit Lean à cette fin. Il présenta cette vision lors du programme Big Proof au Newton Institute, où Kevin Buzzard l'entendit et décida d'essayer Lean pour l'enseignement.
L'abandon du constructivisme dogmatique
Un acte décisif de la communauté Lean fut d'abandonner l'obsession curieuse pour les « preuves constructives » qui avait dominé Rocq durant toute son existence. La philosophie de l'intuitionnisme émergea après le paradoxe de Russell avec des implications particulières pour les nombres réels.
Bien que la théorie des types de Martin-Löf soit reconnaissablement intuitioniste, c'est moins évident pour Rocq. Pourtant, article après article mentionnait « preuve constructive » là où c'était sans pertinence, voire absurde. Cette obsession entrava l'application de Rocq aux mathématiques, laissant le champ libre à Lean.
Au-delà de « propositions comme types »
Le principe « propositions comme types » établit une dualité reliant les signes logiques ∀, ∃, →, ∧, ∨ aux constructeurs de types Π, Σ, →, ×, +. C'est beau, fascinant et théoriquement fructueux, mais ce n'est pas la seule approche existante.
Certains définissent « assistant de preuve » comme un logiciel vérifiant les preuves selon ce principe. Cette définition efface la majorité des recherches du dernier demi-siècle, ne laissant que Rocq, Lean et Agda. Même AUTOMATH n'est pas une instance de propositions comme types.
L'inutilité des objets de preuve
Rocq et Lean incluent le type Prop des propositions, fournissant l'indépendance des preuves : tous les objets de preuve pour une proposition donnée s'évaluent à la même valeur. Ces termes massifs sont donc inutiles, mais conservés malgré tout.
Que les objets de preuve soient superflus fut la découverte clé de Robin Milner pour LCF. Il suffit d'un langage de programmation (ML) fournissant des types de données abstraits. Placez votre noyau de preuve dans un type abstrait, avec les règles d'inférence comme constructeurs, et voilà : les preuves sont vérifiées dynamiquement.
Il est absurde, à l'ère de la saturation mémoire, de gaspiller des dizaines de mégaoctets sur des termes géants qui ne dénotent rien. Cette problématique rejoint les enjeux de compression et d'optimisation qui préoccupent l'ensemble du domaine de l'IA.
Pourquoi choisir Isabelle en 2026 ?
Si vos collègues utilisent Lean, qu'ils possèdent une expertise dans ce système et que vos prérequis essentiels figurent dans les bibliothèques Lean, utilisez évidemment Lean. Mais si vous êtes libre de choisir, plusieurs raisons militent pour Isabelle.
Une automatisation incomparable
Ne vous laissez pas tromper par les discussions sur les « marteaux » comme outils quotidiens : rien n'égale sledgehammer. Cette capacité d'automatisation surpasse largement ce qui existe ailleurs, incluant des intégrations avec l'algèbre informatique.
Cette supériorité en automatisation devient particulièrement pertinente avec l'essor de l'IA générative. Les preuves générées par IA tendent à être désordonnées, mais sledgehammer facilite considérablement leur nettoyage. Puisqu'elles sont bien structurées – du moins avec Claude selon une expérience limitée – elles restent lisibles malgré leur détail souvent excessif.
Lisibilité optimale
Isabelle offre le meilleur choix pour la lisibilité. La transparence ultime n'est pas un objet de preuve vérifiable par ordinateur, mais un texte de preuve qu'un être humain peut réellement lire. De nombreux exemples illustrent cette qualité sur le blog Machine Logic.
Cette lisibilité facilite également l'optimisation et l'analyse du contenu, permettant d'identifier rapidement les opportunités de simplification.
Absence de types dépendants
Pas de niveaux d'univers, pas de bizarreries qui piègent les débutants. Les types dépendants sont d'ailleurs découragés dans mathlib de Lean et dans SSReflect et Mathematical Components de Rocq.
Une difficulté majeure avec les types dépendants : si correctement implémentés, la vérification de types doit être indécidable, car l'égalité est indécidable. Dans les années 90, le consensus bascula vers l'égalité définitionnelle ou intensionnelle pour rendre la vérification décidable. C'est pourquoi T(N+1) et T(1+N) sont des types différents.
Capacités mathématiques avancées sans types dépendants
En 2017, on aurait pu douter des capacités mathématiques d'Isabelle. Il semblait naturel d'imaginer que les types dépendants étaient nécessaires pour gérer les extensions de corps, les nombres p-adiques ou les schémas de Grothendieck.
Des recherches ont démontré le contraire. L'astuce consiste à cesser de forcer tout à être un type. Cette flexibilité architecturale rappelle les approches innovantes en conception matérielle qui remettent en question les paradigmes établis.
L'avenir de la formalisation mathématique
Lean réussit beaucoup de choses correctement et possède le potentiel d'être lisible, supportant même les blocs de preuve imbriqués. Sa communauté d'utilisateurs doit maintenant exploiter ces fonctionnalités, comme le font déjà majoritairement les utilisateurs d'Isabelle.
L'impact de l'intelligence artificielle
L'essor de l'IA accentue ces différences. Les recherches récentes montrent que les modèles de langage peuvent eux-mêmes appeler sledgehammer. L'IA peut également traduire facilement les preuves structurées lisibles d'un assistant de preuve à un autre.
Cette interopérabilité croissante signifie qu'à terme, le choix de l'assistant de preuve deviendra moins crucial. Les collaborations entre géants technologiques accélèrent cette convergence, rendant les écosystèmes plus ouverts.
Cependant, les questions de sécurité des modèles et de manipulation des systèmes IA restent préoccupantes dans ce contexte d'ouverture croissante.
Diversité technologique et innovation
L'histoire de la formalisation mathématique enseigne une leçon fondamentale : les avancées majeures proviennent rarement de la conformité. AUTOMATH, Boyer-Moore, LCF, HOL et Isabelle ont tous apporté des contributions uniques précisément parce qu'ils exploraient des approches différentes.
Réduire le paysage à un seul outil, aussi excellent soit-il, appauvrit l'écosystème de recherche. La diversité des approches stimule l'innovation, favorise la découverte de solutions inattendues et garantit la résilience face aux défis futurs.
Mizar : le grand oublié
Aucun historique de la formalisation mathématique n'est complet sans évoquer Mizar et sa vaste bibliothèque mathématique. Développé en Pologne dès les années 70, Mizar a influencé de nombreux systèmes ultérieurs.
Le langage Isar d'Isabelle emprunte massivement à Mizar, notamment son approche déclarative des preuves qui privilégie la lisibilité. Mizar a démontré qu'une syntaxe proche du langage mathématique naturel pouvait coexister avec une vérification formelle rigoureuse.
Cette contribution mérite reconnaissance et étude, car elle illustre une fois de plus qu'explorer des chemins alternatifs enrichit l'ensemble du domaine.
En conclusion, la question « Pourquoi ne pas simplement utiliser Lean ? » mérite une réponse nuancée. Lean est un excellent outil qui a légitimement conquis une large communauté. Mais l'histoire nous rappelle que la diversité technologique n'est pas un luxe : c'est le moteur même du progrès scientifique. Pour aller plus loin dans votre exploration des assistants de preuve et découvrir comment l'IA peut transformer votre approche de la formalisation mathématique, créez votre compte gratuit sur Roboto.
