AI Agents for the Working Mathematician
AI Agents for the Working Mathematician
Most working mathematicians I talk to or observe have the same<br>relationship with AI: they paste a question into ChatGPT, get something<br>proof-shaped back, feel vaguely impressed or vaguely cheated, and go<br>back to work. This makes sense, especially under the common opinion:
If you ask ChatGPT a few times and it does not solve the problem,<br>then AI can NEVER solve the problem by itself.
This opinion was formed by mathematicians worldwide through long and<br>brutal ChatGPT sessions: read the latest output, send “keep going”, wait<br>for a response, repeat until the entire afternoon is wasted. If the<br>opinion were true, then asking ChatGPT a few times would be the optimal<br>way of using AI to do math — and to be fair, even that is occasionally<br>strong enough to solve real open problems.
But the opinion is wrong (see FAQ). You can use a<br>system that is far more capable, with a much higher chance of success<br>than the standard opinion allows.
Specifically, you can have an autonomous agent that keeps bashing on<br>a conjecture for hours: it keeps track of itself, learns from its<br>mistakes, does not waste its time retrying something already tried, does<br>not waste your time with long wrong proofs, and you can still influence<br>its direction.
I will use some words like token, model, and harness. If you don’t<br>know what they mean, watch the first part of Edward Lockhart’s<br>talk. I recommend it to anyone who has a math background but no idea<br>what these new AI things are.
1 Use Agents
An agent is an AI that uses tools. Here the tools are<br>exactly what you would use on a computer: operating system, Python, a<br>LaTeX compiler, SAGE math, a browser. Agents can interact with the<br>environment and actually “do” things.
Codex is the coding harness from OpenAI. It runs<br>agents on your own computer. A “chat” session in Codex would be an<br>agent. ChatGPT Work , which is different from ChatGPT,<br>is also an agent, and can run on OpenAI’s server. I prefer Codex as one<br>can maintain even tighter control, but if you just want to explore,<br>ChatGPT Work is easier as you don’t even need to download anything.<br>However, this article I will assume people will be using Codex.
What Codex buys you over the chat window:
Files are durable state. Your problem statement,<br>definitions, proved lemmas, failed attempts — they live in a directory,<br>in git if you like. Progress is not lost, you can keep advancing.
You control the context. The agent reads the files<br>you point it at. You have much more control over what agents can do. A<br>clean STATEMENT.md with your exact conventions beats<br>re-explaining notation every conversation.
Tool use. Gurobi to construct counterexamples, SAGE<br>to compute some polynomial, LEAN to formally verify some statement it<br>proved, access to your compute cluster, and tools that help with your<br>computation that you never knew existed.
Long autonomous runs. You can hand it a hard<br>target, leave, and come back to either progress or a precise record of<br>what failed.
Step by step on how to do it.
Use an agent
Codex: Download the Codex program and log in with your ChatGPT<br>account.
ChatGPT Work: Just open the ChatGPT website, and switch it to<br>work.
Set the model to the highest available, currently gpt-5.6-sol<br>ultra.
Replace [STATEMENT] in the prompt below with your exact<br>claim — all quantifiers, your conventions, what is known, and what<br>counts as an answer — then use it on a conjecture you always wanted to<br>solve.
Current task statement
[STATEMENT]
## Success criteria
Partial progress does not count unless it implies exactly the resolution above. In particular, proofs for special classes, reductions to another unproved conjecture, computational verification through any fixed size, and candidate counterexamples without a complete nonexistence certificate are insufficient. If the statement above is ambiguous about what counts as an answer, ask before starting; never resolve ambiguity silently.
## Durable state — create these files before searching
- STATEMENT.md — the exact statement, conventions, and success criteria. Fixed for the whole run; never edit it to fit a result.<br>- REGISTRY.md — one row per approach family: family name, exact claim attempted, exact remaining gap, smallest known obstruction, next decisive test, status.<br>- FAILED.md — every closed route: what was tried, the exact obstruction, the evidence for it, and what would make a retry materially new.<br>- PROVED.md — promoted results only, each with its status label and proof or certificate.
All mathematical work products land in these files, not only in conversation. After any context compaction, re-read these files before continuing; they are the memory, the conversation is not.
## Status vocabulary — literal, never inflated
Every claim carries exactly one label, with these exact meanings:
- candidate — produced by an agent; no checks yet.<br>- self-audited — re-checked only by its own author or context. For...