Lean (assistant de preuve)

Lean est un assistant de preuve et un langage de programmation. Il repose sur le principe de calcul des constructions avec types inductifs.


Lean Theorem Prover

Informations
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 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.

Exemples

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

  1. Hales, « A Review of the Lean Theorem Prover » (consulté le )
  2. Buzzard, « The Future of Mathematics? » (consulté le )

Liens externes

  • Portail de la programmation informatique
  • Portail du logiciel
Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.