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:

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)