I have made a number of contributions to Lean's mathematical library mathlib and beyond. Here is a broad overview; all my (merged and pending) contributions can be found on GitHub.

Statistics and general overview

• since Septembere 2023, I have made 119 commits on mathlib, with 10 pull requests awaiting review
• according to Github's statistics, I was the 6th most prolific contributor (by number of commits)
• new mathematics contributed to mathlib: +1077 lines merged, 350 under review, 670 in the pipeline, over 2000 lines overall
• large number of style and house-keeping changes: splitting large files, adding documentation, renaming misleading lemmas, code clean-up
• I try to review other contributions when I can
• I have recently begun moving material from the sphere eversion project to mathlib: since January 10, I have
• moved about 650 lines of code into mathlib (merged), mostly about topology and differential geometry
• moved 400 further lines (awaiting review in mathlib), also including analysis results
• performed a fair number of maintainance changes in sphere-eversion, including porting the blueprint to Lean 4 names, updating mathlib repeatedly, minimizing imports and adjusting coding style towards mathlib's

New mathematics formalised

Most new mathematics I have formalised is related to Sard's theorem, for instance as a pre-requisite to its proof. This includes the following.

• measure zero subsets of a manifold
• locally Lipschitz maps
• sigma-compact sets
• nowhere dense and meagre sets
• sigma-compact measure zero sets are meagre
• second countable finite-dimensional manifolds are sigma-compact
• local diffeomorphisms have invertible differential

Other mathematics contributions point towards formalising various aspects of differential geometry:

• interior and boundary of a manifold
• real manifolds are locally path-connected
• path-connectedness is preserved under homeomorphisms
• the inverse function theorem on manifolds (including in a "categorical" version, unifying the smooth and analytic settings)
• immersions, submersions and embeddings