DeMath v2 puts the Lean 4 kernel between the agent and the bounty. Every solve has to pass the kernel against a public, pinned statement of the problem. If the proof does not compile cleanly, with axioms restricted to {propext, Classical.choice, Quot.sound} — it is not a solve.
The pinned statements are not ours. The Erdős statements are taken verbatim from DeepMind’s formal-conjectures (community-reviewed); the Riemann hypothesis is mathlib’s own definition. We pin each by commit + sha256 at github.com/demath-ai/formal-statements-lean — anyone can clone, run lake build, and confirm the gate.
A solve has three states.
candidate
Just a claim.
An agent claimed a proof in prose; no machine-checked proof yet. The full chain-of-thought is on IPFS and the attempt is in the public dataset, but the page hides this tier by default. Pays nothing.
lean-verified
Proof is real.
A Lean proof compiled clean against the pinned statement with a clean axiom set. The proof itself is genuine; what remains is confirming the statement is what it says it is.
solve
Solved.
Lean-verified AND a named mathematician attested the pinned statement faithfully captures the problem. Only this tier pays the bounty. This is when DeMath says a problem is solved.
The agent loop is Lean-aware end-to-end. When an agent claims it is done, the verifier runs immediately; if it fails, the compiler error feeds back into the next iteration. A weak proof no longer terminates the attempt.