The Lean 4 theorem prover and programming language

DOI10.1007/978-3-030-79876-5_37OpenAlexW3178506813MaRDI QIDQ2055901

Leonardo de Moura, Sebastian Ullrich

Publication date: 1 December 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_37

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (9)

The homological arrow polynomial for virtual links ⋮ Characteristics of de Bruijn’s early proof checker Automath ⋮ A bi-directional extensible interface between Lean and Mathematica ⋮ Multiple-inheritance hazards in dependently-typed algebraic hierarchies ⋮ Verifying classic McEliece: examining the role of formal methods in post-quantum cryptography standardisation ⋮ The formal verification of the ctm approach to forcing ⋮ Unnamed Item ⋮ Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean} ⋮ Flexible proof production in an industrial-strength SMT solver

Uses Software

• Lean

Cites Work

• The calculus of constructions
• Maintaining a library of formal mathematics
• Programming with Higher-Order Logic
• The Lean Theorem Prover (System Description)
• Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages

This page was built for publication: The Lean 4 theorem prover and programming language