Formalizing Mathematics in Lean
formalization
lean
Contributions to mathlib, the Lean theorem prover’s mathematics library.
An ongoing interest in machine-checked mathematics. I have contributed to mathlib, the Lean theorem prover’s mathematics library:
- Lean’s surreal numbers library
- Lean’s convex optimization library
I have also taught Lean as a week-long class at Mathcamp.