Sovány | |
---|---|
Típusú | Profi asszisztens |
Fejlesztő | Microsoft Research |
Beírva | C++ |
Operációs rendszer | platformközi |
Interfész nyelvek | angol |
Első kiadás | 2013 |
Hardver platform | platformközi |
legújabb verzió | 4,0,0-m4 (2022. március 23. ) |
Engedély | Apache licenc 2.0 |
Weboldal | leanprover.github.io |
A Lean egy interaktív tételbizonyító eszköz . Az induktív típusú konstrukciók számítása alapján . Nyílt forráskódú a GitHubon . A Lean projektet Leonardo de Moura indította el a Microsoft Researchnél 2013-ban [1] .
A Lean-nek van egy felülete, amely megkülönbözteti a többi interaktív tételbizonyítótól. A Lean JavaScriptre fordítható , és elérhető egy webböngészőben . Natív támogatással rendelkezik a Unicode karakterekhez . (Beírhatók LaTeX -szerű szekvenciákkal, például "\times" a "×"-nél.) A Lean széleskörű metaprogramozási támogatással is rendelkezik .
A karcsúsítás felkeltette Thomas Hales és Kevin Bazard matematikusok figyelmét. Hales a "formalabstracts" projektjéhez használja [2] . Bazard a Xena projekthez használja [3] A Xena projekt egyik célja az, hogy átírja az összes tételt és bizonyítást az Imperial College London egyetemi matematika tantervében .
A Xena projekt keretében a sűrített matematika területéről Peter Scholze [4] [5] [6] által kidolgozott komplex bizonyítást formalizálnak .
A természetes számok meghatározása:
induktív nat : Típus | nulla : nat | succ : nat → natA természetes számok összeadási műveletének meghatározása:
definíció add : nat → nat → nat | n nulla := n | n ( succ m ) := succ ( add n m )Példa egy egyszerű bizonyításra.
tétel és_csere : p ∧ q → q ∧ p := tegyük fel h1 : p ∧ q , ⟨ h1.jobbra , h1.balra ⟩Ez a bizonyíték:
tétel és_csere ( p q : Prop ) : p ∧ q → q ∧ p := kezdjük tegyük fel h : ( p ∧ q ), -- tegyük fel, hogy p ∧ q igaz h esetek , -- kivonjuk az egyes propozíciókat a kötőszó felosztásából , -- bontsa fel a cél kötőszót két esetre: bizonyítsa be p és bizonyítsa q külön-külön ismételje meg { feltételezés } vége ![]() |
---|