Lean (proof assistant)

Lean
ParadigmStrict purely functional, dependently typed
FamilyProof assistant
Designed byLeonardo de Moura
DeveloperLean FRO
First appeared2013 (2013)
Stable release
4.26.0  / 13 December 2025 (13 December 2025)
Typing disciplinestatic, strong, inferred
Implementation languageLean, C++
PlatformARM32-64, x86-64
OSCross-platform: Linux, Windows
LicenseApache 2.0
Websitelean-lang.org
Influenced by
ML, Rocq (formerly named Coq), Haskell

Lean is a proof assistant and a functional programming language. It is based on the calculus of constructions with inductive types. It is a free and open-source software project hosted on GitHub. Development is currently supported by the nonprofit Lean Focused Research Organization (FRO).

This article is issued from Wikipedia. The text is available under Creative Commons Attribution-Share Alike 4.0 unless otherwise noted. Additional terms may apply for the media files.