Formalize everything, now!
Two years after arguing for an autoformalizer, an industry has formed and AI has formalized Fermat's Last Theorem. We should now build a formal library of all known mathematics.
Justin Asher
I’m a mathematician working on AI for mathematics and software verification. I’m also interested in the social sciences.
Latest writing
What did the Lean proof of Fermat's Last Theorem formalize?
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.
Numina Fuse
An introduction to my NYC Lean talk on Fuse: parallel agents for formalizing mathematics in Lean, with a readable blueprint of their work.
Talk · NYC Lean
The need for an autoformalizer
The creation of an autoformalizer—a machine that can verify mathematics—would have monumental benefits for both academic research and industrial applications.
LeanExplore: The backbone of agentic mathematics
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
This article discusses a previous attempt at creating a large database of autoformalized mathematics.
Hilbert's 10th problem
We prove that Hilbert's 10th problem has a negative answer using Turing machines, and then mention generalizations and applications to Mazur's conjecture.
Modeling Catan through self-play
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
We motivate and state the basic definitions of infinity categories.
Casas-Alvero conjecture
Let F be a polynomial over a field of characteristic 0 that shares a root with each derivative. Does F(X) = (X - α)^n for some α? We prove that this holds for polynomials of degree n = p^k for p prime.
Ramanujan conjecture
We discuss the main tools used by Deligne in proving the Ramanujan conjecture and how it relates to the Weil conjectures.
Motivating schemes with the Weil conjectures
We state the Weil Conjectures, then give an overview of how Lefschetz theory and étale cohomology can be used to prove them.
Local systems as locally constant sheaves
Let X be a locally simply connected space. We prove that the categories of locally constant sheaves and local systems on X are equivalent.
IU analysis qualifying solutions
These are notes meant to help students at Indiana University pass the analysis qualifying exams.
Categorical coproducts and K-theory
We define products and coproducts for arbitrary categories, then use them to define K-theories.
Cartan-Hadamard theorem for metric spaces
We give a complete proof of the Cartan-Hadamard theorem for metric spaces, filling in details missing from the literature.
Euler characteristic is the index of an operator
Let M be a closed oriented Riemannian manifold. We show that the (analytic) index of a specific Dirac operator equals the Euler characteristic of M.
Gauss-Legendre algorithm
We give a proof sketch for an approximation of π derived from the arithmetic-geometric mean of 1 and √2/2.
The brain age project
A differential geometry-based machine learning algorithm for the brain age problem.