diff --git a/docs/results.json b/docs/results.json index af288be..65757e5 100644 --- a/docs/results.json +++ b/docs/results.json @@ -551,5 +551,16 @@ "size": 0, "condensed-compute-budget": "Avg $6.17 and 31 min/problem", "note": "672/672 Lean problems reported in no-answer mode: 346 answer-placeholder problems and 326 proof-only problems. Total reported cost: $4,144.29. Evaluated against PutnamBench commit b3e08943b1728842194fe2df693f02c763da4294 using Lean v4.31.0 and Mathlib commit fabf563a7c95a166b8d7b6efca11c8b4dc9d911f. Answer-clue comments were removed before prover input. The proof-generation model was not reported; GPT-5.6 was used for placeholder-faithfulness review, followed by manual checking. Two documented compatibility-only input edits preserve the original mathematical statements. For 1974 B1, the submission uses the intended regular-pentagon characterization because the reference answer comment admits repeated-point counterexamples. The Lean proof bundle was shared privately for independent PutnamBench verification." + }, + "Forall (Astrio)": { + "link": "https://www.astriolabs.com/index/forall-lean-agent", + "date-added": "2026-09-24", + "open-data": "NONE", + "num-solved": { + "lean-wsolution": 672 + }, + "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." } }