I gave an agent $250 to formalize Erdős problems
I let Claude Code agents write Lean 4 proofs on a $250 cloud credit. An external verifier, outside the agent's reach, decided what counted.
I gave Claude Code agents a $250 cloud credit and asked them to turn math proofs into Lean 4. I spent $244 of it over 3 and 4 October 2026. Each target was a claim in Google DeepMind's formal-conjectures library, where the proof is a hole. Each session had a time box of 15 to 90 minutes.
The agent is untrusted. It works in its own repository and can edit anything there, including the file that states the question. So I do not believe anything it says.
A second repository, the external verifier, never attaches to an agent session. When the agent finishes, it pushes a commit that starts with "submit". The external verifier finds that commit and throws away the agent's copy of the question. It uses its own frozen copy. Then it runs Comparator, a tool from the Lean team, in a sandbox. A green mark from the external verifier is the only definition of success.
This matters because an agent that grades itself can leave a hole in the proof, or quietly prove an easier question than the one I asked.
I tested the external verifier with one correct proof and seven cheats. It rejected six at once. The seventh printed the external verifier's own success message while it built, and the external verifier searched its log for that message. I changed the external verifier to read Comparator's exit code. That cheat is now a permanent test.
What happened
The external verifier accepted Lean proofs for 26 results that people had already proved on paper. Examples are R(4, 4) = 18, a bound on the Gauss circle problem, and the disproof of a graph conjecture. Short proofs cost about $2 and 30 minutes. Two more known results ended as partial proofs.
I did not solve an open problem. I gave 16 open statements one hour each. Two sessions returned full proofs, and for a moment I thought I had two solved problems. I had not. Other people had proved both months earlier, and the library's "open" label was out of date.
Two problems got deeper runs. For the Catch-Up game, the agent proved the draw claim in Lean for every N up to 16. For squares modulo n, it proved the claim for four kinds of n. Both are partial results, and both problems stay open.
What I learned
- Check the label yourself. I read "open" from the library and did not search for earlier work. Now every problem gets that search before it gets any credit.
- A manager agent did not help here. On one easy problem, a bare agent took about 32 minutes and $2. The setup with a manager and fresh helpers took about 70 minutes and $4.70. The problem was too easy to test the manager fairly.
- The agent did the routine work fast: small cases, computer searches, reductions. Then it stalled at one step that needs a new idea. For Catch-Up, ten attempts in a row ended at the same step.
Code: erdos-lean-formalization and erdos-lean-checker.