Selected recent work
LeanExplore: The backbone of agentic mathematics (2025)
Abstract. The future of mathematics will be unthinkably many agents working together in harmony to expand the known corpus of knowledge. LeanExplore provides a searchable index for them to do this.
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.
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.
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.
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.
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.
© 2024 • Justin Asher