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)