I have made various contributions to Lean's mathematical library mathlib (and beyond). The following is a broad overview; all my (merged and pending) contributions can be found on GitHub. This page was last updated on: January 17th, 2025
New mathematics formalised
Statistics and general overview
- since September 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
I have worked on various pre-requisites to formalising symplectic geometry, including Sard's theorem , the implicit function theorem (in Banach manifolds) and the basics for bordism theory. A number of pre-requisites and related results have already been incorporated into mathlib. A detailed list of my contributions can be found here.
My current activities include contributing to the Carleson project and formalising various analytic results concerning Sobolev spaces, partial differential operators or elliptic regularity estimates.
I have reviewer rights within mathlib.
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.
Other mathematics contributions point towards formalising various aspects of differential geometry: