The Lean Theorem Prover (System Description)

DOI10.1007/978-3-319-21401-6_26zbMath1465.68279OpenAlexW1464569014MaRDI QIDQ3454108

Leonardo de Moura, Floris van Doorn, Jakob von Raumer, Jeremy Avigad, Soonho Kong

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: https://figshare.com/articles/journal_contribution/The_Lean_Theorem_Prover_system_description_/6492815

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (67)

Semantic representation of general topology in the Wolfram language ⋮ A web-based toolkit for mathematical word processing applications with semantics ⋮ Formalizing geometric algebra in Lean ⋮ Equality Checking for General Type Theories in Andromeda 2 ⋮ RustHorn: CHC-Based Verification for Rust Programs ⋮ A language with type-dependent equality ⋮ A certified program for the Karatsuba method to multiply polynomials ⋮ Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis ⋮ A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper) ⋮ Deep Generation of Coq Lemma Names Using Elaborated Terms ⋮ Validating Mathematical Structures ⋮ Formalization of Forcing in Isabelle/ZF ⋮ Aligning concepts across proof assistant libraries ⋮ Voting theory in the Lean theorem prover ⋮ Program logic for higher-order probabilistic programs in Isabelle/HOL ⋮ Hammer for Coq: automation for dependent type theory ⋮ Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge ⋮ Schemes in Lean ⋮ Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types ⋮ Formalizing Galois Theory ⋮ A Coq formalization of Lebesgue integration of nonnegative functions ⋮ A bi-directional extensible interface between Lean and Mathematica ⋮ Validating safety arguments with Lean ⋮ Fundamentals of compositional rewriting theory ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ Homotopy type theory in Lean ⋮ Meaning explanations at higher dimension ⋮ Naïve Type Theory ⋮ What is the point of computers? A question for pure mathematicians ⋮ Multiple-inheritance hazards in dependently-typed algebraic hierarchies ⋮ Abstraction boundaries and spec driven development in pure mathematics ⋮ Elaborating dependent (co)pattern matching: No pattern left behind ⋮ Certifying expressive power and algorithms of reversible primitive permutations with \textsf{Lean} ⋮ A formalization of the change of variables formula for integrals in mathlib ⋮ Formalising the Kruskal-Katona theorem in Lean ⋮ Graded rings in Lean's dependent type theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An extensible equality checking algorithm for dependent type theories ⋮ Verification of the ROS NavFn planner using executable specification languages ⋮ Eliminating dependent pattern matching without K ⋮ Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support ⋮ On a machine-checked proof for fraction arithmetic over a GCD domain ⋮ Unnamed Item ⋮ Friends with Benefits ⋮ Verified Decision Procedures for Modal Logics. ⋮ Declarative Proof Translation (Short Paper) ⋮ Unnamed Item ⋮ Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck} ⋮ From LCF to Isabelle/HOL ⋮ On the Key Dependent Message Security of the Fujisaki-Okamoto Constructions ⋮ Verification of dynamic bisimulation theorems in Coq ⋮ Congruence Closure in Intensional Type Theory ⋮ MODULARITY IN MATHEMATICS ⋮ Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover ⋮ The Isabelle/Naproche natural language proof assistant ⋮ The Lean 4 theorem prover and programming language ⋮ Lean ⋮ MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures ⋮ Experiences from exporting major proof assistant libraries ⋮ Implementing type theory in higher order constraint logic programming ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean} ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ A formalization of Dedekind domains and class groups of global fields ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs

Uses Software

Cites Work

This page was built for publication: The Lean Theorem Prover (System Description)