diff --git a/docs/results.json b/docs/results.json index 65757e5..57c88f2 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": "$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." } }