Formalising the $h$-principle and sphere eversion

TL;DR

This paper formalises the local h-principle in Lean for differential topology, reproving Smale's sphere eversion theorem and advancing the formalisation of geometric mathematics.

Contribution

It provides the first formal proof of the local h-principle for open, ample partial differential relations in Lean, enabling formal verification of complex geometric theorems.

Findings

Formalisation of the local h-principle in Lean

Reproof of Smale's sphere eversion theorem

Foundation for formalising global h-principle in differential topology

Abstract

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 Gromov in 1973 as part of his sweeping effort which greatly generalised many previous flexibility results in topology and geometry. In particular it reproves Smale's celebrated sphere eversion theorem, a visually striking and counter-intuitive construction. Our formalisation uses Theilli\`ere's implementation of convex integration from 2018. This paper is the first part of the sphere eversion project, aiming to formalise the 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 of 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 flavour and not only algebraically-flavoured