roza
Follow
Program = Proof
Lean Library currently studying for a degree at Imperial College
An updated version of miniF2F with lots of fixes and informal statements / solutions.
A formalized proof of Carleson's theorem in Lean
Source code for the Mathematics in Lean tutorial.
The user home repository for the Mathematics in Lean tutorial.
Framework for specifying and proving properties—such as robustness, fairness, and interpretability—of machine learning models using Lean 4.
Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant
Lean 4 programming language and theorem prover
A template for blueprint-driven formalization projects in Lean.