| Udviklet af | Microsoft Research |
|---|---|
| Første version | 2013 |
| Sidste version | 3.4.2 (18. januar 2019) |
| Depositum | https://github.com/leanprover/lean |
| Skrevet i | C ++ |
| Miljø | I browseren eller på tværs af platformen |
| Sprog | engelsk |
| Type | Bevisassistent |
| Licens | Apache 2.0 |
| Internet side | https://leanprover.github.io |
Lean er en bevisassistent og et programmeringssprog . Det er baseret på princippet om beregning af konstruktioner med induktive typer .
Lean har en række bemærkelsesværdige funktioner, der adskiller den fra anden bevisassisterende software . Lean kan samles i JavaScript , hvilket gør det tilgængeligt i en webbrowser . Det understøtter indbygget Unicode- tegn til matematiske symboler, som kan indtastes ved hjælp af genveje, der minder om LaTeX- syntaks (f.eks. "×" opnås ved at skrive "\ times"). Det er også muligt at foretage metaprogrammering på det samme sprog som til konventionel brug. Således, hvis brugeren ønsker at skrive en funktion, der automatisk beviser bestemte sætninger, er det muligt at skrive i Lean en funktion, der genererer de ønskede bevis i Lean.
Lean fangede matematikernes Thomas Hales og Kevin Buzzards opmærksomhed . Hales bruger det til sit Formal Abstracts- projekt . Buzzard bruger det til Xena-projektet , hvis mål er at omskrive alle sætninger og bevis i Imperial College Londons Undergraduate Mathematics Program i Lean .
Her er hvordan naturlige tal defineres i Lean:
inductive nat : Type | zero : nat | succ : nat → natHer er definitionen af tilføjelse for hele tal:
definition add : nat → nat → nat | n zero := n | n (succ m) := succ(add n m)Her er et simpelt bevis i Lean:
theorem and_swap : p ∧ q → q ∧ p := assume h1 : p ∧ q, ⟨h1.right, h1.left⟩Her er det samme bevis ved hjælp af taktik:
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