8000
Stars
A Lean 4 companion to Lawvere and Schanuel's Conceptual Mathematics (2nd ed)
Lean 4 programming language and theorem prover
Lean theorem proving interface which feels like pen-and-paper proofs.
The "batteries included" extended library for the Lean programming language and theorem prover
Templates for getting started with Verso
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.