| Dezvoltat de | Microsoft Research |
|---|---|
| Prima versiune | 2013 |
| Ultima versiune | 3.4.2 (18 ianuarie 2019) |
| Depozit | https://github.com/leanprover/lean |
| Scris in | C ++ |
| Mediu inconjurator | În browser sau pe mai multe platforme |
| Limbi | Engleză |
| Tip | Asistent de dovadă |
| Licență | Apache 2.0 |
| Site-ul web | https://leanprover.github.io |
Lean este un asistent de probă și un limbaj de programare . Se bazează pe principiul calculului construcțiilor cu tipuri inductive .
Lean are o serie de caracteristici notabile care îl diferențiază de alte programe de asistență pentru dovezi . Lean poate fi compilat în JavaScript , făcându-l accesibil într-un browser web . Suportă în mod nativ caractere Unicode pentru simboluri matematice, care pot fi introduse folosind comenzi rapide care amintesc de sintaxa LaTeX (de exemplu, „×” se obține tastând „\ times”). De asemenea, este posibil să faceți meta-programare utilizând același limbaj ca și pentru utilizarea convențională. Astfel, dacă utilizatorul dorește să scrie o funcție care dovedește automat anumite teoreme, este posibil să scrieți în Lean o funcție care generează dovezile dorite în Lean.
Lean a atras atenția matematicienilor Thomas Hales și Kevin Buzzard . Hales îl folosește pentru proiectul său Formal Abstracts . Buzzard îl folosește pentru Proiectul Xena , unul dintre obiectivele acestuia fiind de a rescrie în Lean fiecare teoremă și dovadă a programului de matematică de la Imperial College London .
Iată cum sunt definite numerele naturale în Lean:
inductive nat : Type | zero : nat | succ : nat → natIată definiția adunării pentru numerele întregi:
definition add : nat → nat → nat | n zero := n | n (succ m) := succ(add n m)Iată o dovadă simplă în Lean:
theorem and_swap : p ∧ q → q ∧ p := assume h1 : p ∧ q, ⟨h1.right, h1.left⟩Iată aceeași dovadă folosind tactici:
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