Verdikta Bounties has run a series of math bounties where two AI models (one from OpenAI, one from Anthropic, 50% weight each) grade a written proof against a weighted rubric, and an on-chain escrow pays if the score clears a threshold. I went through all ten completed ones. The numbers tell a more interesting story than "AI can or can't check proofs".
The data
| Bounty | Theorem | Threshold | Result |
|---|---|---|---|
| #114 | Fermat's little theorem + compute 2^52 mod 53 | 85% | 99% |
| #116 | Pigeonhole principle + card problem | 77% | 99% |
| #119 | A tree with n vertices has n-1 edges | 88% | 98% |
| #120 | Infinitely many primes | 83% | 99% |
| #128 | A set of n elements has 2^n subsets | 84% | 99% |
| #131 | Chain rule | 85% | 99% |
| #132 | det(AB) = det(A)det(B) | 82% | 97% |
| #133 | Continuous bijection, compact to Hausdorff, is a homeomorphism | 78% | 99% |
| #134 | Homomorphisms map identity to identity | 83% | 99% |
| #135 | Euler's formula V - E + F = 2 | 80% | 79% (rejected), then 99% |
Eleven submissions in total. Ten passed, every one of them with 97% to 99%. The single rejection missed the bar by one point.
Observation 1: a ceiling effect means the jury isn't discriminating
When every accepted proof lands between 97 and 99, the grade carries almost no information. These are some of the most famous proofs in undergraduate mathematics: Euclid's primes, the pigeonhole principle, induction on trees. A model has seen thousands of clean versions of each, so it is comparing a submission against a memorized template, not checking a chain of reasoning from scratch.
That is the hard part of proof verification for LLMs, and it isn't arithmetic. A model is best at recognizing a proof that looks like a proof it has seen. It is weakest exactly where verification matters: a step that is missing but expected, so the model's own memory quietly fills the gap.
Observation 2: the one rejection caught a 200-year-old gap
The rejected Euler submission is the most informative data point in the set. Its rubric weighted the complete proof at 0.45, worked examples at 0.25, and the theorem statement and a convexity note at 0.15 each. The published jury reasoning (on IPFS, linked from the bounty page) says:
- gpt-5.6-sol leaned to funding. It noted a small error, a mislabeled torus example (a torus has V - E + F = 0, not 2), but credited the valid alternative spanning-tree proof and the correct examples.
- claude-sonnet-5 flagged the induction-on-faces argument as the weakest element: a "hand-waved treatment" of critical cases and assumptions about removable faces in a triangulated polyhedron.
That objection is not a model quirk. It is the classic flaw in Cauchy's 1813 proof of Euler's formula: you flatten the polyhedron, triangulate, and remove triangles one at a time, but whether every removal keeps the invariant depends on the order, and a careless order breaks it. Imre Lakatos built his book Proofs and Refutations (1976) around exactly this proof and its counterexamples. One model found the gap that took mathematicians decades to name properly. The other didn't weigh it.
Observation 3: averaging dilutes the model that is right
With 50/50 weighting, the stricter model's correct objection was averaged with the lenient model's approval, and the submission landed at 79% against an 80% threshold. The final written justification even recommended "FUND" while the score fell short. The prose summary and the payout rule disagreed.
For proofs this matters more than for essays. In an essay, two graders disagreeing about tone can reasonably meet in the middle. In a proof, one valid objection to one step is decisive. A proof with a gap is not 79% correct, it is incomplete. Averaging treats a logical gap like a matter of taste.
I saw the same split on a non-math Verdikta bounty I submitted to myself: one model scored 84 and the other 65 on the same text. Disagreement between models is normal. The question is what the aggregation does with it.
What I think works better for math bounties
- Grade rigor with a minimum, not an average. Let style and exposition be averaged, but score the "complete proof" criterion as the lower of the two models, or require an explicit list of gaps from each model and fail if either finds one it can name.
- Ask for a proof the models haven't memorized. Instead of "prove there are infinitely many primes", use a variant: primes of the form 4k+3, or a specific modular computation the submitter must justify step by step. Variants push the jury from recognition to verification.
- Add an error-finding task. Give a proof with one planted flaw (like the order problem in Cauchy's argument) and pay for locating it. Models are better critics than they are generators of rigor, and that tests the useful skill.
- Separate computation from proof. #114 asked for 2^52 mod 53. By Fermat's little theorem the answer is 1, since 53 is prime. That kind of claim can be checked mechanically, so let a deterministic check grade it, and save the models for the reasoning.
The takeaway
Multi-model consensus helps: a second, different model is what caught the Euler gap at all. But consensus by averaging wastes that advantage on proofs. The models were not the weak link here. The 97-99% ceiling and the 79% near miss both point at the same thing: math bounties need rubrics and aggregation designed for proofs, where a single correct objection should count for more than a polite average.
All data from the public bounty pages and their jury reasoning on bounties.verdikta.org.
Top comments (0)