Sovány

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  ( 2013 )
Hardver platform platformközi
legújabb verzió 4,0,0-m4 (2022. március 23. ) ( 2022-03-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 .

Alkalmazás

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 .

Kódpéldák

A természetes számok meghatározása:

induktív nat : Típus | nulla : nat | succ : nat nat

A 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

Lásd még

Jegyzetek

  1. Karcsú . Letöltve: 2021. szeptember 30. Az eredetiből archiválva : 2021. október 18..
  2. Formális absztraktok
  3. Mi az a Xena projekt? | Xena
  4. Kevin Hartnett. A Proof Assistant átugrik a Big League Math-ba . Quanta (2021. július 28.). Letöltve: 2021. október 1. Az eredetiből archiválva : 2021. szeptember 30.
  5. David Castelvecchi. A matematikusok üdvözlik a számítógéppel segített bizonyítást a „nagy egyesülés” elméletében // Természet. - 2021. - Kt. 595. - P. 18-19. - doi : 10.1038/d41586-021-01627-2 .
  6. A Liquid Tensor Experiment befejezése . Lean közösségi blog (2022. július 15.). Letöltve: 2022. július 17.

Linkek