Lean combined a small proof-checking kernel, an expressive dependent type theory, interactive proof development and extensible automation in one open platform intended for formalized mathematics as well as verification.
At CADE-25 on 7 August 2015, Leonardo de Moura and collaborators presented Lean as a new open-source theorem prover with a small trusted kernel based on dependent type theory and an explicit goal of bridging interactive and automated theorem proving. The Springer CADE-25 proceedings containing the system description were published on 30 July 2015. The official Lean history records the first repository commit in July 2013 and the official Lean 0.1 release in June 2014; because those earlier records are month-precision only, this Event uses the exact CADE presentation date as its canonical public anchor.
The system became a durable substrate for large formal mathematical libraries and later learning-based theorem provers, making its pre-2016 introduction essential historical context for the Chronicle's later Lean-centered AI4Math milestones.
Significance rationale: Lean established a new dependent-type proof-assistant platform explicitly designed to combine interactive theorem proving with automation, laying the technical foundation for the later Lean/mathlib ecosystem and a major share of modern AI-assisted formal mathematics.
—
—
Springer published the CADE-25 proceedings containing the Lean system description, documenting the architecture, goals and use of the prover in formal mathematics.
The official CADE presentation, official project history and preserved open-source Lean 3 repository make the early system lineage and implementation directly inspectable. The exact June 2014 Lean 0.1 release day is not inferred from month-only historical metadata.
No corrections recorded.
