ERDŐS
The coin that proves math.
Erdős put cash bounties on his hardest problems. are still unclaimed (about ). An AI is going after them, live.
The prover is NEAR AI's open-source Lean agent, paid for by trading fees. Lean checks every proof, so you can verify it yourself.
Bounties from erdosproblems.com, via the teorth/erdosproblems database.
| –problems attempted | –proofs verified by Lean | –open problems cracked | –compute spent |
Latest
See every problem- Waiting for the feed.
How it works
A problem goes in
Google DeepMind's formal-conjectures project has stated 786 Erdős problems in Lean 4, each tagged open or solved. The agent works through them from a queue.
The agent writes a proof
NEAR AI's open-source prover writes Lean, runs it, reads the errors and tries again. Every turn streams to this site.
Lean checks it
A proof counts only if Lean compiles it with no
sorryand only the standard axioms. The file is published, so anyone can re-check it.
Where NEAR comes in
NEAR AI built the prover.
NEAR AI is the AI lab of NEAR, co-founded by Illia Polosukhin, a co-author of “Attention Is All You Need”. It open-sourced the Lean agent this project runs. That agent solved all 672 PutnamBench problems (the Putnam, the hardest undergraduate math competition, formalized in Lean) for $111.85 in total, a median of $0.04 per problem.
Sources: the nearai/putnambench-deepseek README and NEAR's post of Sep 4, 2026.
NEAR AI Cloud will run it.
The agent's model is DeepSeek V4.1 Flash, and NEAR AI Cloud is where it is meant to be served. Model compute is the project's running cost.
Waiting for the live feed to report the model and provider.
NEAR fees pay for it.
$ERDOS launches on pump.fun paired with NEAR instead of SOL, so every buy of $ERDOS buys NEAR. Creator fees arrive in NEAR and pay for the agent's compute. More trades, more math.
NEAR on Solana, mint 3ZLekZYq2qkZiSpnSvabjit34tUkjSwD1JFuW9as9wBG
Verify it yourself
You don't have to trust us, the model or this site. Lean re-checks any proof on your own machine. Every proved problem has its own page with these commands filled in.
It passes if Lean prints no errors and the axiom line lists only propext, Classical.choice and Quot.sound. If you see sorryAx, the proof is incomplete.
FAQ
What's an Erdős problem?
Paul Erdős (1913–1996) posed hundreds of problems, many with cash prizes, and many are still open. erdosproblems.com, run by Thomas Bloom, tracks them.
What does “verified by Lean” mean?
Lean 4 is a proof checker. A proof that compiles with no sorry and only the standard axioms is correct for the statement as written. No trust in the AI is needed: the check is mechanical, and you can run it yourself.
What if a statement was formalized wrong?
That can happen. A formal statement can itself contain a mistake, and then a valid proof proves the wrong thing. Before we announce that an open problem is proved, a human checks that the proof doesn't exploit a mis-formalized statement.
How does NEAR fit in?
NEAR AI built the prover. NEAR AI Cloud is where it is meant to run; the live status above says what serves it right now. And $ERDOS is paired with NEAR on pump.fun, so every buy buys NEAR and creator fees, paid in NEAR, fund the compute.
Does ERDŐS win the prize money?
No. Erdős prizes are for the mathematician who solves the problem; this project publishes its proofs openly.
Where do the fees go?
Creator fees from $ERDOS trades arrive in NEAR and pay for the agent's model compute. The compute spent so far is the live total at the top of this page.