Homepage with Search Bar
Welcome!

I am a mathematician working on building mathematical artificial intelligence



Selected recent work

Introducing Vantage: Towards highly-parallelized autoformalization (2025)

Abstract.   This article reports progress on building an autoformalizer, introducing the Vantage Project. Experiments highlighted LLM retrieval capabilities but also reasoning/verification limits, motivating Vantage's approach: using LLMs to suggest content for a Lean 4 knowledge base, verified through iterative checks. This graph-based KB, enabling parallel formalization, aims to create a "vantage point" for automated mathematics.

Read web article →

The need for an autoformalizer (2024)

Abstract.   I argue that the creation of an autoformalizer—a machine that can verify mathematics—would have monumental benefits for both academic research and industrial applications. I then discuss how one could be created.

Read web article →

Modeling Catan through self-play (2024)

Abstract.   I taught a neural network how to play the board game Catan using supervised learning via self-play. The resulting model achieved an intermediate level of play.

Read web article →

Infinity categories (2024)

Abstract.   In this note, we answer the question "What is an infinity category?", explaining the definition in terms of simplicial categories, ordinary category theory, and homotopy theory.

Read web article →

The Ramanujan conjecture (2023)

Abstract.   We discuss some of the main tools used by Deligne in proving the Ramanujan conjecture. These are notes from a talk, so I do not include most proofs.

Read web article →