In differential topology and geometry, the h-principle is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existence of a solution come from algebraic topology.

We describe a formalisation in Lean of the local h-principle for first-order, open, ample partial differential relations. This is a significant result in differential topology, originally proven by M. Gromov in 1973 as part of his sweeping effort to re-examine and greatly generalise many previous flexibility results in topology and geometry. In particular this reproves Smale’s celebrated sphere eversion theorem, a visually striking and counter-intuitive construction. Our formalisation uses Theillière’s implementation of convex integration from 2018.

This paper is the first part of the sphere eversion project, which aims to formalise the \emph{global} version of the h-principle for open and ample first order differential relations, for maps between smooth manifolds. Our current local version for vector spaces is the main ingredient for this proof, and is sufficient to prove the titular corollary of the project. From a broader perspective, the goal of this project is to show that one can formalise advanced mathematics with a strongly geometric flavor and not only algebraically flavored mathematics.