Leaderboard
Difficulty-weighted contribution to the unsorry Math corpus. Source: unsorry git.
2,075
Verified proofs
1,767
Attributed (explicit)
308
Inferred (git)
730
Terminal runs
| Rank | Contributor | Score |
|---|---|---|
| 🥇 | OH@ohdearquant | 216,950 |
| 🥈 | CH@chat-bit-01 | 163,025 |
| 🥉 | CG@cgbarlow | 97,745 |
| #4 | RU@ruvnet | 46,900 |
| #5 | PE@perttu | 32,160 |
| #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 / sympy1,169 proofs · 100% of 382 runs
lean / decide306 proofs
openrouter / unknown160 proofs
claude / opus59 proofs · 54% of 24 runs
codex / unknown39 proofs · 6% of 72 runs
openai / leanstral-260321 proofs · 0% of 201 runs
gemini / gemini-3.1-pro-preview7 proofs · 0% of 2 runs
manual / gpt-5.54 proofs
claude / sonnet1 proofs
claude / unknown1 proofs