Opírat se

Lean je interaktivní nástroj pro dokazování teorémů . Na základě počtu konstrukcí s indukčními typy. Jedná se o open source hostovaný na GitHubu . Projekt Lean zahájil Leonardo de Moura v Microsoft Research v roce 2013 [1] .

Lean má rozhraní, které jej odlišuje od ostatních interaktivních dokazovačů teorémů. Lean lze zkompilovat do JavaScriptu a je k dispozici ve webovém prohlížeči . Má nativní podporu pro znaky Unicode . (Lze je psát pomocí sekvencí podobných LaTeXu , jako "\times" pro "×".) Lean má také rozsáhlou podporu metaprogramování .

Aplikace

Lean přitáhl pozornost matematiků Thomase Halese a Kevina Bazarda. Hales to používá pro svůj projekt „formalabstracts“ [2] . Bazard jej používá pro projekt Xena [3] Jedním z cílů projektu Xena je přepsat všechny teorémy a důkazy v bakalářských osnovách matematiky na Imperial College London .

V rámci projektu Xena je formalizován komplexní důkaz z oblasti kondenzované matematiky vyvinutý Peterem Scholzem [4] [5] [6] .

Příklady kódu

Definice přirozených čísel:

indukční nat : Typ | nula : nat | succ : nat → nat

Definice operace sčítání pro přirozená čísla:

definice add : nat → nat → nat | n nula := n | n ( succ m ) := succ ( přidat n m )

Příklad jednoduchého důkazu.

teorém and_swap : p ∧ q → q ∧ p := předpokládat h1 : p ∧ q , ⟨ h1.right , h1.left ⟩

Toto je důkaz:

věta and_swap ( p q : Prop ) : p ∧ q → q ∧ p := begin předpokládat h : ( p ∧ q ), -- předpokládat p ∧ q je pravdivé případy h , -- extrahovat jednotlivé výroky ze spojky split , -- rozdělte cílovou spojku na dva případy: dokažte p a dokažte q samostatně opakujte { předpoklad } konec

Viz také

• Interaktivní nástroj pro dokazování teorémů

Poznámky

1. ↑ Naklonit se . Získáno 30. září 2021. Archivováno z originálu dne 18. října 2021. (neurčitý)
2. ↑ Formální abstrakta
3. ↑ Co je projekt Xena? | Xena
4. ↑ Kevin Hartnett. Důkaz Assistant dělá skok do Big League Math . Quanta (28. července 2021). Získáno 1. října 2021. Archivováno z originálu dne 30. září 2021. (neurčitý)
5. ↑ David Castelvecchi. Matematici vítají počítačově podporovaný důkaz v teorii „velkého sjednocení“ // Příroda. - 2021. - Sv. 595. - S. 18-19. - doi : 10.1038/d41586-021-01627-2 .
6. ↑ Dokončení experimentu kapalinového tenzoru . Blog štíhlé komunity (15. července 2022). Staženo: 17. července 2022. (neurčitý)

Odkazy

• Lean web
• The Natural Number Game – Interaktivní výukový program, který se naučí štíhle

Tematické stránky	otevřený rozbočovač