Lean Programming Language

Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code

Lean lets you write precise, verifiable code and formal proofs.