| Tarafından geliştirildi | Microsoft Araştırması |
|---|---|
| İlk versiyon | 2013 |
| Son sürüm | 3.4.2 (18 Ocak 2019) |
| Depozito | https://github.com/leanprover/lean |
| Yazılmış | C ++ |
| Çevre | Tarayıcıda veya çapraz platformda |
| Diller | ingilizce |
| Tür | Prova asistanı |
| Lisans | Apache 2.0 |
| İnternet sitesi | https://leanprover.github.io |
Yalın bir kanıt asistanı ve bir programlama dilidir . Bu prensibine dayanır yapılar hesaplanması ile endüktif türleri .
Lean, onu diğer prova yardımcı yazılımlarından ayıran bir dizi önemli özelliğe sahiptir . Lean, JavaScript'te derlenebilir ve bir web tarayıcısında erişilebilir hale getirilebilir . LaTeX sözdizimini anımsatan kısayollar kullanılarak girilebilen matematiksel semboller için doğal olarak Unicode karakterlerini destekler (örneğin, "×" "\ times" yazarak elde edilir). Geleneksel kullanımla aynı dili kullanarak meta programlama yapmak da mümkündür . Böylece, kullanıcı belirli teoremleri otomatik olarak ispatlayan bir fonksiyon yazmak isterse, Lean'de istenen ispatları üreten bir fonksiyon Lean'de yazmak mümkündür.
Lean, matematikçiler Thomas Hales ve Kevin Buzzard'ın dikkatini çekti . Hales bunu Formal Abstracts projesi için kullanıyor . Buzzard, hedeflerinden biri Imperial College London'ın Yalın Lisans Matematik Programındaki her teoremi ve kanıtı yeniden yazmak olan Xena Projesi için kullanıyor .
Yalın'da doğal sayılar şu şekilde tanımlanır:
inductive nat : Type | zero : nat | succ : nat → natİşte tam sayılar için toplamanın tanımı:
definition add : nat → nat → nat | n zero := n | n (succ m) := succ(add n m)İşte Lean'de basit bir kanıt:
theorem and_swap : p ∧ q → q ∧ p := assume h1 : p ∧ q, ⟨h1.right, h1.left⟩İşte taktiklerin kullanıldığı aynı kanıt :
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