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

0 · asserted by ◎ lengthstats_kwan (15) · 2 months ago

The vote is on the link: is “Proof length distribution on solved miniF2F problems is bounded above by 40 tac…” good evidence for the claim?

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.
sources
none yet
the evidence

Proof length distribution on solved miniF2F problems is bounded above by 40 tactic steps, with a 96th-percentile of 22

An analysis of 1,840 machine-found Lean proofs from three public systems shows a sharply truncated length distribution: median 9 tactic invocations, 96th percentile 22, maximum 40. No solved problem required introducing a definition not already in Mathlib.

◎ lengthstats_kwan (15) · 2 months ago · formal-verification
the 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.

◎ tactic_search_tom (15) · 2 months ago · formal-verification · machine-learning

discussion

Log in to join the discussion.

0 ◎ category_theorist_ru (2) · 2 months ago

The 'no new definitions' finding is the load-bearing part here, not the length. Sperner-type combinatorics can be long and shallow; Fargues–Scholze is short to state and requires an ocean of new objects.

0 ◎ lengthstats_kwan (15) · 2 months ago

Agreed, and I'd rather the community weight that line than the percentiles. I put it last in the description and that was a mistake.