The sphere eversion project

This project is a formalization of 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)