AI Agents for Mathematicians: Beyond Chat-Based Prompting
Why agentic harnesses like Codex outperform chat prompting for tackling open math conjectures, with durable state and strict verification labels.
Most mathematicians treat AI as a chatbot: paste a problem, get a proof-shaped answer, and conclude that if a few prompts don't crack it, the model never will. This piece argues that conclusion mistakes a shallow usage pattern for a fundamental limit — agentic, tool-using harnesses like OpenAI's Codex or ChatGPT Work behave very differently from a chat window.
Instead of losing context every turn, an agent works from durable files: a fixed problem statement, a registry of approaches tried, a log of failed routes with their exact obstructions, and a file of promoted results. It can call Python, LaTeX, SAGE, or LEAN, run for hours unattended, and resume cleanly after context resets because the files — not the conversation — are the memory.
A key mechanism is a strict status vocabulary for claims: candidate, self-audited, verifier-backed, promoted, and independently audited, each requiring a specific verification step before a result can be built upon. Combined with subagent orchestration — up to six concurrent agents pursuing genuinely diverse approaches, then fresh agents auditing the results — this turns loose prompting into a disciplined, falsifiable research process. For engineers, it's a concrete template for using LLMs on open-ended, hard problems where correctness and traceability matter more than a quick answer.