Læne

Lean er et interaktivt teorembevisværktøj . Baseret på beregningen af ​​konstruktioner med induktive typer. Det er open source hostet på GitHub . Lean-projektet blev lanceret af Leonardo de Moura hos Microsoft Research i 2013 [1] .

Lean har en grænseflade, der adskiller den fra andre interaktive teorembevisere. Lean kan kompileres til JavaScript og er tilgængelig i en webbrowser . Det har indbygget understøttelse af Unicode-tegn . (De kan skrives ved hjælp af LaTeX -lignende sekvenser, såsom "\times" for "×".) Lean har også omfattende metaprogrammeringsunderstøttelse .

Ansøgning

Lean tiltrak sig opmærksomhed fra matematikerne Thomas Hales og Kevin Bazard. Hales bruger det til sit "formalabstracts"-projekt [2] . Bazard bruger det til Xena-projektet [3] Et af målene med Xena-projektet er at omskrive alle teoremer og beviser i bacheloruddannelsen i matematik ved Imperial College London .

Inden for rammerne af Xena-projektet formaliseres et komplekst bevis fra området for kondenseret matematik udviklet af Peter Scholze [4] [5] [6] .

Kodeeksempler

Definition af naturlige tal:

induktiv nat : Type | nul : nat | succ : nat → nat

Definition af additionsoperationen for naturlige tal:

definition tilføje : nat → nat → nat | n nul := n | n ( succ m ) := succ ( tilføje n m )

Et eksempel på et simpelt bevis.

teorem and_swap : p ∧ q → q ∧ p := antag h1 : p ∧ q , ⟨ h1.højre , h1.venstre ⟩

Dette er beviset:

sætning og_bytte ( p q : Prop ) : p ∧ q → q ∧ p := start antag h : ( p ∧ q ), - antag, at p ∧ q er sande tilfælde h , - udtræk de individuelle propositioner fra konjunktionssplitningen , -- opdel målkonjunktionen i to tilfælde: bevis p og bevis q separat gentag { antagelse } ende

Se også

• Et interaktivt teorembevisværktøj

Noter

1. ↑ Magt . Hentet 30. september 2021. Arkiveret fra originalen 18. oktober 2021. (ubestemt)
2. ↑ Formelle abstrakter
3. ↑ Hvad er Xena-projektet? | Xena
4. ↑ Kevin Hartnett. Proof Assistant gør spring til Big League Math . Quanta (28. juli 2021). Hentet 1. oktober 2021. Arkiveret fra originalen 30. september 2021. (ubestemt)
5. ↑ David Castelvecchi. Matematikere hilser computerstøttet bevis velkommen i teorien om 'grand unification' // Nature. - 2021. - Bd. 595. - S. 18-19. - doi : 10.1038/d41586-021-01627-2 .
6. ↑ Afslutning af væsketensoreksperimentet . Lean community blog (15. juli 2022). Hentet: 17. juli 2022. (ubestemt)

Links

• Lean hjemmeside
• The Natural Number Game - En interaktiv tutorial til at lære lean

Tematiske steder	åbent nav