This project is a formalization the proof of existence of sphere eversions using the Lean theorem prover, mainly developed at Microsoft Research by Leonardo de Moura. More precisely we formalized the full h-principle for open and ample first order differential relations, and deduce existence of sphere eversions as a corollary.
The main motivations are:
- Demonstrating the proof assistant can handle geometric topology, and not only algebra or abstract nonsense. Note that Fabian Immler and Yong Kiam Tan already pioneered this direction by formalizing Poincaré-Bendixon, but this project has much larger scale.
- Exploring new infrastructure for collaborations on formalization projects, using the interactive blueprint.
- Producing a bilingual informal/formal document by keeping the blueprint and the formalization in sync.
The main statements that we formalized appear in main.lean. In particular the sphere eversion statement is:
theorem Smale : -- There exists a family of functions `f t` indexed by `ℝ` going from `𝕊²` to `ℝ³` such that ∃ f : ℝ → 𝕊² → ℝ³, -- it is smooth in both variables (for the obvious smooth structures on `ℝ × 𝕊²` and `ℝ³`) and (cont_mdiff (𝓘(ℝ, ℝ).prod (𝓡 2)) 𝓘(ℝ, ℝ³) ∞ ↿f) ∧ -- `f 0` is the inclusion map, sending `x` to `x` and (f 0 = λ x, x) ∧ -- `f 1` is the antipodal map, sending `x` to `-x` and (f 1 = λ x, -x) ∧ -- every `f t` is an immersion. ∀ t, immersion (𝓡 2) 𝓘(ℝ, ℝ³) (f t)