Mathematics, machine reasoning, and the work of making ideas precise.
No essays in this topic yet.
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.
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
LeanExplore provides a searchable index of Lean packages, enabling AI agents to search for declarations by name, code, and informal meaning.
The creation of an autoformalizer—a machine that can verify mathematics—would have monumental benefits for both academic research and industrial applications.
This article discusses a previous attempt at creating a large database of autoformalized mathematics.
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.
We prove that Hilbert's 10th problem has a negative answer using Turing machines, and then mention generalizations and applications to Mazur's conjecture.
We motivate and state the basic definitions of infinity categories.
We discuss the main tools used by Deligne in proving the Ramanujan conjecture and how it relates to the Weil conjectures.
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.
We state the Weil Conjectures, then give an overview of how Lefschetz theory and étale cohomology can be used to prove them.
These are notes meant to help students at Indiana University pass the analysis qualifying exams.
Let X be a locally simply connected space. We prove that the categories of locally constant sheaves and local systems on X are equivalent.
We define products and coproducts for arbitrary categories, then use them to define K-theories.
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.
We give a complete proof of the Cartan-Hadamard theorem for metric spaces, filling in details missing from the literature.
We give a proof sketch for an approximation of π derived from the arithmetic-geometric mean of 1 and √2/2.
A differential geometry-based machine learning algorithm for the brain age problem.