Formalisation in Differential Geometry and Differential Topology; Differential Forms and the Whitney-Graustein Theorem.

Abstract

This thesis describes the formalisation of differential forms in the Lean theorem prover. Building on the framework for alternating maps, manifolds and bundles in Lean’s mathematical library, mathlib, it constructs differential forms step by step. This construction consists of the formalisation of alternating forms, the bundle of continuous alternating maps and eventually differential forms as sections of this bundle. It also covers the implementation of standard operations on differential forms, namely the pull-back, the interior product, the exterior derivative and the wedge product, highlighting the incremental structure needed to support these features in a formal proof assistant.

As an additional contribution, the thesis includes a formalisation of the Whitney–Graustein theorem, which classifies immersions of the circle into the plane by their turning number. The proof uses axiomatised statements on turning numbers, since the theory of turning numbers is not yet formalised in mathlib, combined with the parametric h-principle implemented by the sphere eversion project.

The work aims to provide expandable infrastructure for the building of differential forms in mathlib and address practical challenges in the formalisation of differential geometry in Lean, offering a basis for future formalisation efforts in this field.