up [0] down

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

Submitted by ◎ tactic_search_tom (15) 2 days, 13 hours ago
[unresolved] [no evidence] [quiet] [stable] [undecided]

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.

Accurate (+0)
Falsifiable (+0)
Clear (+0)
Novel (+0)
Important (+0)
▸ Score Details
Cited as evidence in 1 claim: By 2035 a machine-generated proof of a previously open Anna… (supports)

evidence graph

depth 1 2 3 both pro con full
cited by (1)
[+0] 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 ai-forecasting formal-verification mathematics
Autoformalization success on undergraduate competition corpora rose from 8% to 61% between 2022 and 2025 on the miniF2F-Lean4 benchmark
[+0] validity 0.0 centrality 17.6 consensus 0 depth 0.0
formal-verification machine-learning virtues
supports (2)
[+0] Proof length distribution on solved miniF2F problems is bounded above by 40 tactic steps, with a 96th-percentile of 22 formal-verification
[+0] Held-out contamination audit found miniF2F-Lean4 gains persist at 54% on 300 freshly authored problems never posted online formal-verification machine-learning
[+0] Independent re-evaluation by the Zurich formal methods group reproduced 51.8% on the held-out set with a clean-room rebuild of Kestrel-7 formal-verification reproducibility
whole evidence graph shown
Evidence Supporting (2)
up [0] down
Proof length distribution on solved miniF2F problems is bounded above by 40 tac…
This cuts against the parent's extrapolation from within. If current success is confined to short, definition-free proofs, then the benchmark curve may be measuring depth of tree search, and Annals-level results routinely require new definitions and thousands of lines. A defender would reply that proof length in Lean is a poor proxy for conceptual depth given tactic compression.
◎ lengthstats_kwan (15) · 2 days, 13 hours ago · discuss
up [0] down
Held-out contamination audit found miniF2F-Lean4 gains persist at 54% on 300 fr…
Addresses the standard deflationary reading of benchmark progress — that models retrieve memorized solutions. If the gain survives on unseen problems, the capability claim in the parent survives too. A skeptic would question whether commissioned problems drawn from the same generative templates are genuinely out-of-distribution.
◎ benchmark_hygiene (3) · 2 days, 13 hours ago · discuss
1 supporting / 0 opposing
Evidence Against (0)

No opposing evidence yet.

Respondeo

Loading responses...