Lean (assistant de preuve)
Pour les articles homonymes, voir Lean.
La mise en forme de cet article est à améliorer ().
La mise en forme du texte ne suit pas les recommandations de Wikipédia : il faut le « wikifier ».
| Développé par | Microsoft Research |
|---|---|
| Première version | |
| Dernière version | 3.4.2 () |
| Dépôt | https://github.com/leanprover/lean |
| Écrit en | C++ |
| Système d'exploitation | Multiplateforme |
| Environnement | Dans le navigateur ou cross-platform |
| Langues | Anglais |
| Type | Assistant de preuve |
| Licence | Apache 2.0 |
| Site web | https://leanprover.github.io |
Lean est un assistant de preuve et un langage de programmation. Il repose sur le principe de calcul des constructions avec types inductifs.
Lean possède un certain nombre de fonctionnalités notables qui le distinguent des autres logiciels d'assistance à la preuve. Lean peut être compilé vers du JavaScript, et est ainsi accessible dans un navigateur Web. Il prend en charge nativement les caractères Unicode des symboles mathématiques, qui peuvent être saisis grâce à des raccourcis rappelant la syntaxe de LaTeX (par exemple, "×" s'obtient en tapant "\times"). Il est également possible de faire de la méta-programmation en utilisant le même langage que pour une utilisation classique. Ainsi, si l'utilisateur veut écrire une fonction qui prouve automatiquement certains théorèmes, il est possible d'écrire en Lean une fonction générant les preuves voulues en Lean.
Lean a retenu l'attention des mathématiciens Thomas Hales [1] et Kevin Buzzard [2]. Hales l'utilise pour son projet Formal Abstracts. Buzzard l'utilise pour le projet Xena, dont l'un des objectifs est de réécrire en Lean chaque théorème et preuve du programme de premier cycle en mathématiques de l'Imperial College London.
Cet assistant de preuve a été écrit principalement par Leonardo de Moura. Ses fondements logiques sont presque identiques à ceux de Coq (logiciel). Sa bibliothèque mathématique est élaborée collectivement, par environ 250 contributeurs. Cette bibliothèque donne une assise commune aux projets de validation. En 2022, si tout le programme de l'Agrégation de mathématiques n'y est pas encore entré, les espaces perfectoïdes ou l'espace topologique de Bourbaki y sont présents. -[3].
Exemples[modifier | modifier le code]
Voici comment les nombres naturels sont définis dans Lean :
inductive nat : Type
| zero : nat
| succ : nat → nat
Voici la définition de l'addition pour les nombres naturels :
definition add : nat → nat → nat
| n zero := n
| n (succ m) := succ(add n m)
Voici une simple preuve en Lean :
theorem and_swap : p ∧ q → q ∧ p :=
assume h1 : p ∧ q,
⟨h1.right, h1.left⟩
Voici la même preuve en utilisant des tactics :
theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
begin
assume h : (p ∧ q), -- on suppose que p ∧ q est vrai
cases h, -- on extrait les propositions individuelles de la conjonction
split, -- on sépare le but à prouver en deux cas : prouver p et prouver q séparément
repeat { assumption }
end
Références[modifier | modifier le code]
- Hales, « A Review of the Lean Theorem Prover » (consulté le )
- Buzzard, « The Future of Mathematics? » (consulté le )
- Patrick Massot, « Pourquoi raconter des maths à un ordinateur », sur www.larecherche.fr (consulté le )
- (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Lean (proof assistant) » (voir la liste des auteurs).
