Mager

Lean är ett interaktivt verktyg för att bevisa teorem . Baserat på kalkylen för konstruktioner med induktiva typer. Det är öppen källkod värd på GitHub . Lean-projektet lanserades av Leonardo de Moura på Microsoft Research 2013 [1] .

Lean har ett gränssnitt som skiljer det från andra interaktiva teoremprovare. Lean kan kompileras till JavaScript och finns tillgängligt i en webbläsare . Den har inbyggt stöd för Unicode-tecken . (De kan skrivas med hjälp av LaTeX -liknande sekvenser, som "\times" för "×".) Lean har också omfattande metaprogrammeringsstöd .

Applikation

Lean uppmärksammades av matematikerna Thomas Hales och Kevin Bazard. Hales använder det för sitt "formalabstracts"-projekt [2] . Bazard använder det för Xena-projektet [3] Ett av målen med Xena-projektet är att skriva om alla teorem och bevis i matematikläroplanen vid Imperial College London .

Inom ramen för Xena-projektet formaliseras ett komplext bevis från området för kondenserad matematik utvecklat av Peter Scholze [4] [5] [6] .

Kodexempel

Definition av naturliga tal:

induktiv nat : Typ | noll : nat | succ : nat → nat

Definition av additionsoperationen för naturliga tal:

definition lägg till : nat → nat → nat | n noll := n | n ( succ m ) := succ ( lägg till n m )

Ett exempel på ett enkelt bevis.

sats och_byte : p ∧ q → q ∧ p := antag h1 : p ∧ q , ⟨ h1.höger , h1.vänster ⟩

Detta är beviset:

theorem and_swap ( p q : Prop ) : p ∧ q → q ∧ p := börja anta h : ( p ∧ q ), -- anta att p ∧ q är sanna fall h , -- extrahera de individuella propositionerna från konjunktionen split , -- dela upp målkonjunktionen i två fall: bevisa p och bevisa q separat upprepa { antagande } slut

Se även

• Ett interaktivt verktyg för att bevisa teorem

Anteckningar

1. ↑ Luta . Hämtad 30 september 2021. Arkiverad från originalet 18 oktober 2021. (obestämd)
2. ↑ Formella sammandrag
3. ↑ Vad är Xena-projektet? | Xena
4. ↑ Kevin Hartnett. Proof Assistant gör hoppa till Big League Math . Quanta (28 juli 2021). Hämtad 1 oktober 2021. Arkiverad från originalet 30 september 2021. (obestämd)
5. ↑ David Castelvecchi. Matematiker välkomnar datorstödda bevis i teorin om "stor enande" // Nature. - 2021. - Vol. 595. - S. 18-19. - doi : 10.1038/d41586-021-01627-2 .
6. ↑ Slutförande av vätsketensorexperimentet . Lean community-blogg (15 juli 2022). Hämtad: 17 juli 2022. (obestämd)

Länkar

• Lean hemsida
• The Natural Number Game- En interaktiv handledning för att lära dig lean

Tematiska platser	öppet nav