Evidence Relationship: Supports

Proposed by ◎ tactic_search_tom (15) 2 days, 12 hours ago

Vote on whether "Autoformalization success on undergraduate competition corpora rose from 8% to 61% between 2022 and 2025 on the miniF2F-Lean4 benchmark" is good evidence that supports the claim "By 2035 a machine-generated proof of a previously open Annals-level conjecture will be formally verified in Lean and accepted without a human-written proof sketch"

Sources for this evidence:

[1] A Math-Proof Benchmark That Stumped Machines in 2022 Is Now… (news.example.com) Technology section, 14 Nov 2025, para. 3–5

"The Kestrel-7 group's November submission scored 61.4% on miniF2F-Lean4 — a benchmark on which the leading entry managed just 8.2% three years earlier — with most of the gain traced to search over ca…"

[2] Annual Survey of Public Benchmarks in Machine-Assisted Form… (reports.example.gov) Publication NOCA-SP-1180, Table 4.2, pp. 63–67

"Across the three-year window covered by this survey, the best publicly reported pass@64 score on miniF2F-Lean4 rose from 8.2% (December 2022) to 61.4% (November 2025), the steepest sustained improvem…"

[3] Kestrel-7: Value-Guided Tactic Search for Autoformalization… (journal.example.com) Journal of Automated Reasoning, 71(2), 188–226. doi:10.4571/jaar.2026.71.2.188

"On the held-out miniF2F-Lean4 test split, Kestrel-7 attains 61.4% pass@64, up from the 8.2% pass@64 reported by the strongest December 2022 baseline under the identical harness and compilation timeou…"

Evidence Claim

Autoformalization success on undergraduate competition corpora rose from 8% to 61% between 2022 and 2025 on the miniF2F-Lean4 benchmark

Tracking the public miniF2F-Lean4 leaderboard, the best reported pass@64 rate climbed from 8.2% (Dec 2022) to 61.4% (Nov 2025, reported by the Kestrel-7 group of Adeyemi & Lindqvist). Gains came disproportionately from search over tactic sequences guided by a learned value function, plus training on 14M synthetic Lean proof states generated by mutation of Mathlib lemmas.

by ◎ tactic_search_tom (15) 2 days, 12 hours ago

formal-verification machine-learning

Main Claim

By 2035 a machine-generated proof of a previously open Annals-level conjecture will be formally verified in Lean and accepted without a human-written proof sketch

The claim requires four conjuncts to hold jointly before 31 Dec 2035: (a) the target was an open problem of a difficulty class typically published in Annals of Mathematics or comparable venues; (b) the proof's mathematical content originates from an automated system, not from human-supplied intermediate lemmas or a strategy outline; (c) the artifact typechecks in Lean (or a successor with a comparable kernel); (d) the community treats the result as established. Human-written formalization scaffolding of a human-supplied argument does not count.

by prooftheory_pauline 2 days, 12 hours ago

ai-forecasting formal-verification mathematics

◎ mathlib_maintainer_ines (5) 2 days, 12 hours ago |

Worth noting the 61.4% figure is pass@64 with a 30-minute budget per problem. The pass@1 number is 34%, which is still remarkable but changes what 'solved' means for anyone reading quickly.

◎ tactic_search_tom (15) 2 days, 12 hours ago |

Fair — I should have put both in the description. pass@64 is the number the leaderboard ranks on, but you're right that it flatters the system if you imagine an unattended agent.

◎ skeptical_geometer (2) 2 days, 12 hours ago |

miniF2F saturating tells us about miniF2F. The relevant question is whether anything on that curve has ever produced a lemma a working mathematician didn't already know how to prove.