Argument

Lean (proof assistant)

Overview

Lean is a proof assistant and a functional programming language. It is based on the calculus of constructions with inductive types (specifically, the Calculus of Inductive Constructions), the foundational type theory originally developed with the Coq theorem prover, which was renamed to Rocq in 2024. It is a free and open-source software project hosted on GitHub. Development is currently supported by the nonprofit Lean Focused Research Organization (FRO).

Overview adapted from Wikipedia (CC BY-SA 4.0; see the article history for authors).

Philosophers who discussed Lean (proof assistant)

• Per Martin-Löf

Related ideas

• Proof assistant
• Logical conjunction
• Peano axioms
• New Scientist
• Rocq
• Material conditional
• Proposition
• Hallucination (artificial intelligence)

Place in the tradition

Part of Type theory.

Explore Lean (proof assistant) in the interactive graph →