Blog
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.
The need for an autoformalizer
November 2024
The creation of an autoformalizer—a machine that can verify mathematics—would have monumental benefits for both academic research and industrial applications.
Modeling Catan through self-play
August 2024
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.
Hilbert's 10th problem
January 2024
We prove that Hilbert's 10th problem has a negative answer using Turing machines, and then mention generalizations and applications to Mazur's conjecture.
Infinity categories
January 2024
We motivate and state the basic definitions of infinity categories.
Ramanujan conjecture
October 2023
We discuss the main tools used by Deligne in proving the Ramanujan conjecture and how it relates to the Weil conjectures.
Casas-Alvero conjecture
September 2023
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.
Motivating schemes with the Weil conjectures
August 2023
We state the Weil Conjectures, then give an overview of how Lefschetz theory and étale cohomology can be used to prove them.
IU analysis qualifying solutions
August 2023
These are notes meant to help students at Indiana University pass the analysis qualifying exams.
Categorical coproducts and K-theory
May 2023
We define products and coproducts for arbitrary categories, then use them to define K-theories.
Local systems as locally constant sheaves
May 2023
Let X be a locally simply connected space. We prove that the categories of locally constant sheaves and local systems on X are equivalent.
Euler characteristic is the index of an operator
May 2023
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.
Cartan-Hadamard theorem for metric spaces
December 2022
We give a complete proof of the Cartan-Hadamard theorem for metric spaces, filling in details missing from the literature.
Gauss-Legendre algorithm
October 2022
We give a proof sketch for an approximation of π derived from the arithmetic-geometric mean of 1 and √2/2.
The brain age project
2020
A differential geometry-based machine learning algorithm for the brain age problem.