Formalising the h-principle and sphere eversion
summary
Formalisation in Lean of the local h‑principle for first‑order, open, ample partial differential relations proves Smale’s sphere eversion as a corollary, using Thillière’s convex integration and following Mélanie Taylor’s 2018 simplification. The project produces a reusable library (a loops API and constructions for concatenation and convex hull arguments), totals 15,000 lines of Lean and drives 140+ pull requests to mathlib, covers vector‑space cases and is extended to manifolds, and the mechanised proof checks and composes as expected.
AI-written summary · about