How a Budgeted AI Pipeline Refactored Lean Proofs

Lean is a programming language and proof assistant: a proof is written in a form that software can check against a precise theorem. The Lean Refactor Arena challenged entrants to improve proofs of theorems that already had working proofs. A successful refactor had to leave each theorem statement unchanged and compile on the toolchains specified for that problem. The scoring also rewarded shorter proof text and fewer “heartbeats,” Lean’s measure of elaboration work—the effort required to process a proof.

Bobber Cheng’s report describes a hosted-model entry evaluated on 60 final problems. Its central question was practical: could a system make useful improvements while spending no more than US$3 per problem? The entry scored 86.31 points on the final board, compared with 33.33 for the reference proofs, and placed eighth at the deadline. The score combines proof-length reduction, heartbeat reduction and compatibility across listed toolchains; it is not a measure of how much mathematical knowledge the system discovered.

A compiler in the loop

The pipeline used different models for different jobs. GPT-6.1 Sol handled early sessions and style rewriting; GPT-6.1 Terra handled later sessions and additional attempts; Gemini 4 Argon reviewed proposed edits and helped repair them. The author says these choices were based on tests in the team’s own harness, comparing measured performance with cost—not on a general claim that these models are best for proof work.

Rather than accept a model’s suggestion at face value, the system tested candidate proofs. Its gate checked that the theorem statement stayed intact, screened for disallowed constructs, and required compilation on at least as many of the problem’s listed toolchains as the current proof. It also checked for unfinished proof placeholders and compared candidate and current versions using a paired measurement. Candidates that failed checks, timed out or did not clear the acceptance rule were rejected.

The pipeline also used model-free rewrite stages. These applied programmatic changes—such as simplifying patterns or trying alternative proof steps—and kept an edit only when it passed the same kind of checks. Some rules were developed before the final benchmark was released. Other passes and a later post-processing stage were developed or switched on after release, using work on final-benchmark problems. That distinction matters when interpreting the score.

What the results show

The uploaded run cost US$166.33 at list prices across all 60 problems, or an average of US$2.772 per problem; the report gives a maximum of US$2.874 in that run. Its three full runs produced scores from 85.709 to 86.009 on the team’s meter before the final post-processing. The final board score was 86.31.

Most of the score gain came early: the report says the first stage accounted for 90.8–92.2% of the improvement over reference proofs in the three runs. Later model sessions added a smaller amount, while review, the tail sessions and style rewriting contributed little in those runs. Programmatic stages frozen before release added about 0.88–0.96 points. Additional passes built or enabled after release added 0.26 points in one run, and the post-processing stage added 0.30 points, both measured on the final problems themselves.

These figures suggest that, in this particular setup, repeated model suggestions filtered through compilation and measurement could improve existing proofs within the stated budget. They do not show that the models independently proved new theorems, nor that the workflow will perform similarly on other libraries, languages or tasks.

Important caveats

The strongest caution is benchmark exposure. Although the later rewrite rules do not contain problem names or stored proof text, their development drew on research runs and proof comparisons involving final-benchmark problems. The authors explicitly describe the resulting measurements as “in sample.” Their contribution therefore cannot be treated as an independent test of how those rules would perform on unseen problems.

The report also notes that it is not fully reproducible in the sense of producing identical output every time: model sampling and timing affect results, and even model-free stages can vary with compile times. The three full runs cover only a limited spread, and many development comparisons were based on small samples or single draws. In addition, the paper is a preprint and is primarily an account by the system’s creator. The reported leaderboard and internal checks are informative, but they are not independent replication. The findings support a specific engineering result—a carefully gated competition pipeline—not a broad guarantee about AI-generated proofs.