Skip to content

Forall astrio leaderboard addition #357

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 1 commit into from
Sep 24, 2026
Merged

Forall astrio leaderboard addition #357

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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 @@ -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."
}
}
Loading