Leaderboard
Updated 18 days ago · may be lagging upstreamDifficulty-weighted contribution to the unsorry Math corpus, plus dispatch credit for landing others’ proofs. Source: unsorry git. How scores are calculated
4,755
Verified proofs
4,446
Attributed (explicit)
308
Inferred (git)
399
Terminal runs
Top contributors
| Rank | Contributor | Score |
|---|---|---|
| 🥇 | CG@cgbarlow | 314,900 |
| 🥈 | OH@ohdearquant | 297,175 |
| 🥉 | CH@chat-bit-01 | 288,045 |
| #4 | RU@ruvnet | 46,900 |
| #5 | PE@perttu | 29,975 |
| #6 | AD@adam91holt | 5,075 |
| #7 | BI@binto | 2,125 |
| #8 | RA@Rauxon | 250 |
| #9 | YA@yarcles | 125 |
Model distribution
Verified proofs by provider/model. python / sympy is the deterministic (zero-LLM) solver.
python / sympyPorygon2,373 proofs
lean / ringHoopa1,119 proofs
lean / decideMetagross653 proofs
openrouter / unknownUnown160 proofs
claude / opusAlakazam63 proofs · 21% of 61 runs
codex / unknownPorygon-Z39 proofs · 5% of 75 runs
openai / leanstral-2603Reuniclus21 proofs · 0% of 201 runs
gemini / gemini-3.1-pro-previewHydreigon7 proofs · 0% of 2 runsclaude / fable5 proofs · 82% of 11 runs
manual / gpt-5.5Mewtwo4 proofs
claude / sonnetGardevoir1 proofs
claude / unknownMew1 proofs