The Lean 4 theorem prover and programming language

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

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)

Cites Work

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

Cited In (22)

• Schematic program proofs with abstract execution. Theory and applications
• Machine learning and information theory concepts towards an AI mathematician
• Characteristics of de Bruijn’s early proof checker Automath
• Flexible proof production in an industrial-strength SMT solver
• The formal verification of the ctm approach to forcing
• Formalising the Kruskal-Katona theorem in Lean
• The homological arrow polynomial for virtual links
• Algorithm and abstraction in formal mathematics
• Formalising analysis in Lean: compactness and dimensionality
• A bi-directional extensible interface between Lean and Mathematica
• Maude2Lean: theorem proving for Maude specifications using Lean
• Iscalc: An Interactive Symbolic Computation Framework (System Description)
• Chaining extensionality lemmas in Lean's mathlib
• Transforming optimization problems into disciplined convex programming form
• Voting theory in the Lean theorem prover
• Title not available (Why is that?)
• Verified reductions for optimization
• Specification and verification of a linear-time temporal logic for graph transformation
• Machine-learned premise selection for Lean
• Multiple-inheritance hazards in dependently-typed algebraic hierarchies
• Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean}
• Verifying classic McEliece: examining the role of formal methods in post-quantum cryptography standardisation

Uses Software

• Lean

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• The Lean Theorem Prover (System Description) 👍 👎
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) 👍 👎
• The higher-order prover Leo-III 👍 👎
• LEAN: An intermediate language based on graph rewriting 👍 👎
• Voting theory in the Lean theorem prover 👍 👎
• Logic programming as a basis for lean automated deduction 👍 👎
• Automated Technology for Verification and Analysis 👍 👎

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2055901)