- First-Derivative Test (2024, with Patrick Massot and Floris van Doorn)
- Equivalence between one-point compactification of $\mathbb R$ and the projective line (2024, with Oliver Nash)

Mathlib contributions
My selected contributions to Mathlib, the library of formalized mathematics for the proof assistant Lean: