What is it about?

The goal of this project is to formalize the proof of existence of sphere eversions using the Lean theorem prover, mainly developed at Microsoft Research by Leonardo de Moura. More precisely we want to formalize 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:

Exploring and helping

The best way to get started is to read the blueprint introduction, either in pdf or online. Then have a look at the dependency graph, paying special attention to blue items. Blue items are items that are ready to be formalized because their dependencies are formalized. For lemmas, a blue border means the statement is ready for formalization, and a blue background means the proof is ready for formalization.

Once you spotted something to work on, make sure to discuss in on Zulip before writing code. Once you formalized something, make sure the blueprint is still up to date, since it needs to evolve to its bilingual document final state.