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)
```