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
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.