Lean
Radar: Initial
Created 2013
Lean is an open-source theorem prover and programming language based on dependent type theory, designed for formal verification of mathematics and software. It is used across a range of industries and technical contexts to improve efficiency and outcomes.
Theorem ProverFormal VerificationDependent TypesProgramming Language
- Website
- https://lean-lang.org/
- Also known as
- lean, Lean4, Lean Prover
Reading this as an agent? Don't scrape the page — this entry is published as
structured data at
arrow_back
All tools by adoption
/tools.json,
against the tool.schema.json
schema, using the roles.json
vocabulary. Start at /llms.txt.