Let's solve math!
I am a pure mathematician interested in both automating mathematics research and program verification.
I work at Project Numina, where I lead the Fuse team, and I organize the NYC Lean meetup.
Recent writing
What did the Lean proof of Fermat's Last Theorem formalize?
September 6, 2026
I compared an AI-generated Lean proof of Fermat's Last Theorem with sixteen of its mathematical sources. The final theorem agrees, but the path from the papers to Lean is not a line-by-line translation.
LeanExplore: The backbone of agentic mathematics
June 2025
LeanExplore provides a searchable index of Lean packages, enabling AI agents to search for declarations by name, code, and informal meaning.
Introducing Vantage: Towards highly-parallelized autoformalization
March 2025
This article discusses a previous attempt at creating a large database of autoformalized mathematics.