I am a co-founder of the Northwestern Undergraduate Lean Lab (NULL), a collaborative space for undergraduates to learn Lean. Visit our website to find out more!
Formalized the impossibility of various straightedge and compass constructions. Joint with Fabrizio Barroera, Riccardo Brasca, and Dana Zilberberg. Mathlib PR expected late 2025.