Skip to content

Add Fable 5.1 Max Rocq leaderboard result #359

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
GeorgeTsoukalas merged 3 commits into from
Oct 5, 2026
Merged

Add Fable 5.1 Max Rocq leaderboard result #359

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2d1c3c0
Add Fable 5.1 Max Rocq leaderboard result
GeorgeTsoukalas Oct 5, 2026
7810b21
Simplify Fable result note and retain closed-source classification
GeorgeTsoukalas Oct 5, 2026
b92433d
Simplify Fable compute budget to $45/task
GeorgeTsoukalas Oct 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions docs/results.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -562,5 +562,16 @@
"size": 0,
"condensed-compute-budget": "Mean $3.52 actor-side cost/problem; median $2.49",
"note": "Reported 672/672 Lean wsolution proofs using Claude Opus 5 at xhigh reasoning; 662 accepted in round 1 and 10 in round 2. Actor-side cost: $2,364.39 total; reviewer and infrastructure costs not reported. Lean v4.33.1; statements based on PutnamBench commit f423c17. Evaluated harness is not public and the model is proprietary; proofs and submission evidence were shared privately."
},
"Fable 5.1 Max": {
"link": "https://github.com/yaqub1971/PutnamBench_ROCQ",
"date-added": "2026-10-05",
"open-data": "NONE",
"num-solved": {
"coq-wsolution": 8
},
"size": 0,
"condensed-compute-budget": "$45/task",
"note": "Eight Rocq proofs reported by Yaqub Ali using Fable 5.1 Max: 1962 A2, A4, A5, A6, B2, B5, B6, and 1963 A2. Five use existing statements; 1962 A2, A6, and B5 use corrected formalizations documented in issue #358. Rocq 9.1.0, MathComp 2.5, MathComp-Analysis 1.16.0, Coquelicot 3.4.4; benchmark baseline 4dbe26ef21563af851eedaeb82d936fe1f94fc52; reviewed proof commit f82e7770f18883b05d26eba33089c9d39844ca02. Public proof files and verification workflow."
}
}
Loading