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. This page was last updated on: October 27th, 2025

Statistics and general overview

• since September 2023, I have made 920 commits on mathlib, with 80 pull requests awaiting review
• according to Github's statistics, I was the 5th most prolific contributor over this time span (by number of commits)
• new mathematics contributed to mathlib: 8000 lines merged, further 6000 under review
• large number of style and house-keeping changes: splitting large files, adding documentation, renaming misleading lemmas, code clean-up, removing technical debt
• I review other contributions regularly. Since May 2024, I am part of the mathlib reviewers group. Since October 2025, I am a mathlib maintainer.
• I have helped with the maintenance of the sphere eversion project. I have moved 1400 lines of code (in analysis, topology and differential geometry) into mathlib, with another 200 under review. Other changes include porting the blueprint to Lean 4 names, updating for changes to mathlib and adjusting the coding style towards mathlib.

Differential geometry contributions

I have made a number of contributions to mathlib's differential geometry, relating to a few linked themes.

• existence and uniqueness of the Levi-Civita connection (with Patrick Massot)

  Building on Sébastien Gouezel's definition of Riemannian manifolds, we define affine connections on a vector bundle. We prove the classification of affine connections over a trivial bundle and are working on defining the induced Ehresman connection. We also prove the existence and uniqueness of the Levi-Civita connection (on a Riemannian manifold), also known as the fundamental theorem of Riemannian geometry. The proof of uniqueness is complete; existence is close to completion.
  This project comprises about 7000 lines of code so far: about 3000 have been merged already, the remainder is awaiting mathlib review or will eventually be merged. This project is where the metaprogramming work on elaborators originated.

• formalised the foundations of bordism theory, up to the definition of unoriented bordism groups (and most of the proof that they form an abelian group)

  Some particular contributions include

  • defining the interior and boundary of a manifold,
  • proving the disjoint union of equi-dimensional manifolds is a manifold,
  • computing the interior and boundary of disjoint unions, products, and of the interval,
  • defining a notion of "smooth manifold with boundary but no corners", and
  • defining singular n-manifolds and unoriented bordisms.

  The basic prerequisites are already merged into mathlib; about 1000 lines are still unmerged (since they require a nice definition of embedded submanifolds).

  I have proven the reflexivity and symmetry, but not (yet) transitivity of the bordism relation (as this would require the collar neighbourhood theorem and gluing of manifolds, both of which are a significant amount of work).

• formalised smooth immersions, embeddings and submanifolds in Lean.

  The correct definition of smooth embeddings (suitable for Banach manifolds with corners) is different from the standard textbook definition, but reduces to it in finite dimensions over a complete field. This project is work in progress (at 2000-3000 lines already); it will include proofs that compositions of immersions/smooth embeddings are smooth embeddings, as well as various standard constructions.
  A clean definition of "smooth manifold with boundary but no corners" will use this, so this is necessary for merging my bordism theory work above.

• formalising smooth submersions: I am supervising Samantha Naranjo Guevara, who will define submersions and prove the regular value theorem for her master's thesis.
• formalising the Morse-Sard theorem

  This is a cornerstone of differential topology (and a special case of the Sard-Smale theorem, which features in my PhD research a lot). I have formalised the reduction from manifolds to normed spaces; Yury Kudryashov and I are now slowly working on Moreira's generalisation of Sard's theorem (on normed spaces). Some contributions include sigma-compact sets, nowhere dense and meagre sets, a theory of local diffeomorphisms and the measure zero filter on a manifold.

• the inverse function theorem on manifolds (including in a "categorical" version, unifying the smooth and analytic settings)

Contributions to the Carleson project

While I have written several hundred lines of new code for the Carleson project, my biggest contribution has been of a different kind: generalising Jim Portegies' proof of the Marcinkiewicz real interpolation theorem to also apply to functions into the extended non-negative real numbers $\overline{\mathbb{R}}$. To encompass both the standard setting and this one, we invented a new abstraction of ENormed spaces (which includes normed spaces and $\overline{\mathbb{R}}$). I generalised Jim's proof to this setting (rewriting and cleaning up about 5000 lines of Lean code). This work also included generalising many definitions and lemmas from mathlib that were used; this resulted in about 2500 lines of code modified in mathlib.

Metaprogramming

I have made various contributions to different kinds of meta-programming tasks

• tactic writing: with Arend Mellendijk and Heather Macbeth, I have rewritten the field_simp tactic from ground up. The new algorithm is more predictable, robust and faster (particularly in complex cases).
• linters: Damiano Testa and I are the main contributors to mathlib's syntax linters. I also spent a significant amount of time rewriting mathlib's text-based linters from Python to Lean (and then to proper syntax linters).
• elaborators: Patrick Massot and I have written custom elaborators to easy working in differential geometry. These automate the conversion from a dependent to a non-dependent function (as used for talking about smoothness of sections of a vector bundle), and allow inferring the model with corners in many contexts. These changes improve readability, allow writing code faster and may even speed up the code. Part of this work is merged already, others are under review. Overall, this amounts to about 1000 lines of meta code, with additional 2000 lines of tests.

Mathlib infrastructure

I have helped to create mathlib's new review and triage dashboard. After Johan Commelin wrote an initial prototype, I jumped in and became the main author. As of September 2025, the overall code comprises 4500 lines of Python code, as well as 1000 lines of shell scripts, graphql queries etc. I have authored about 90% of these.
The dashboard provides an overview of all incoming contributions requests to mathlib, allows tracking their overall status and helps to find an appropriate reviewer for each of them. It has changed how many maintainers and reviewers work. Maintaining and further improving this tool is one of the focuses of the new mathlib initiative, and I am very grateful Bryan Chen is now maintaining it.