My proposal Formalizable Mathematics has been recommended for funding by the Simons Foundation for a 2026-2031 Travel Support for Mathematicians grant.
My selected contributions to Mathlib, the library of formalized mathematics for the proof assistant Lean:
- First and Second Derivative Tests (2024-2025, with Patrick Massot, Floris van Doorn, Jireh Loreaux, and Eric Wieser)
- Equivalence between one-point compactification of $\mathbb R$ and the projective line (2024, with Oliver Nash)
- One-point compactification of Euclidean space is homeomorphic to the sphere (2025, with Oliver Nash)