Collaborative projects

Online collaborative projects I am involved in, including formalization efforts in Lean and community-maintained mathematical databases. Launch years are approximate (taken from the repository creation date).

Active

2026Optimization problems — A collection of open optimization problems in mathematics, each tracked with current bounds and references. [code]

2025Erdős problems — A community database recording and tracking the status of the problems catalogued at erdosproblems.com. [code]

2024Exponent pair database — A community-maintained database of exponent pairs and related exponents in analytic number theory, together with the deductions relating them. [code]

2024Prime Number Theorem And… (PNT+) — A Lean formalization of the prime number theorem and related results in analytic number theory. [code]

Completed or inactive

2026Mathlib at ICERM 2026 (Stieltjes integral) — A Mathlib fork developed during the May 2026 ICERM meeting, formalizing the Riemann–Stieltjes integral.

2025Analysis I Lean companion — A Lean companion to the textbook Analysis I, formalizing its results and exercises. [code]

2025Estimates — A proof-of-concept tool for automatically proving or verifying asymptotic estimates in analysis. [code]

2024Equational theories — A collaborative project mapping the implications between equational theories of magmas. [code]

2023Polynomial Freiman–Ruzsa conjecture (PFR) — A Lean formalization of the proof of the polynomial Freiman–Ruzsa conjecture. [code]