From 2d1c3c0075978f18c5274f00d50dfc99771ab43c Mon Sep 17 00:00:00 2001 From: George Tsoukalas Date: Mon, 5 Oct 2026 14:23:53 -0500 Subject: [PATCH 1/3] Add Fable 5.1 Max Rocq leaderboard result --- docs/results.json | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/docs/results.json b/docs/results.json index 65757e5..9c0c8ee 100644 --- a/docs/results.json +++ b/docs/results.json @@ -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": "Estimated $45/task; 1-2 hours/proof", + "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; independent maintainer compilation pending. Evaluated agent/harness code and open model weights were not provided." } } From 7810b21ff591afcdeae75fa0d381a1c686c63c9f Mon Sep 17 00:00:00 2001 From: George Tsoukalas Date: Mon, 5 Oct 2026 14:27:38 -0500 Subject: [PATCH 2/3] Simplify Fable result note and retain closed-source classification --- docs/results.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/results.json b/docs/results.json index 9c0c8ee..22d2c7d 100644 --- a/docs/results.json +++ b/docs/results.json @@ -572,6 +572,6 @@ }, "size": 0, "condensed-compute-budget": "Estimated $45/task; 1-2 hours/proof", - "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; independent maintainer compilation pending. Evaluated agent/harness code and open model weights were not provided." + "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." } } From b92433d2b706a769c37ee4b9e057835a4e44d030 Mon Sep 17 00:00:00 2001 From: George Tsoukalas Date: Mon, 5 Oct 2026 14:30:00 -0500 Subject: [PATCH 3/3] Simplify Fable compute budget to $45/task --- docs/results.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/results.json b/docs/results.json index 22d2c7d..57c88f2 100644 --- a/docs/results.json +++ b/docs/results.json @@ -571,7 +571,7 @@ "coq-wsolution": 8 }, "size": 0, - "condensed-compute-budget": "Estimated $45/task; 1-2 hours/proof", + "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." } }