Skip to content
◈ALB Atlas

Lean Alive

Lean
KindProgramming language
Appeared2013
StatusAlive
CreatorLeonardo de Moura / Microsoft Research
FamilyML
Sourceleanprover.github.io ↗

The theorem prover mathematicians actually adopted — Lean 4 is both proof assistant and programming language, and mathlib keeps growing.

Created by Leonardo de Moura

Leonardo de Moura's Lean (2013) — a theorem prover that became a language — powers mathlib, the largest formalized mathematics library, and is increasingly used for verified systems.\n\nLean 4 (2021) is a practical language; it is the intersection of mathematics and programming where the field's frontier sits.

Sources

  1. leanprover.github.io/
  2. en.wikipedia.org/wiki/Lean_(proof_assistant)