Lean for the Curious Mathematician 2023
Kyle Miller - UCSC Mathematics
Description: personal website
e-mail: [email protected]
I am a postdoc at the mathematics department of the University of Paris-Saclay , working with Patrick Massot working on formalized mathematics in the Lean Theorem Prover . I am a maintainer of its mathematical library mathlib , and my latest project was the sphere eversion project . In this project we formalized an important result in differential topology, namely Gromov's h-principle for first-order differential relations using a technique called convex integration .
To try Lean, I recommend the online book Mathematics in Lean . Or check out these other ways of learning Lean .
Lean for the Curious Mathematician 2023
Kyle Miller - UCSC Mathematics