Lean Compilation Overstates Formalization Accuracy by Up to 29.5 Points

Lean accepts a declaration if it is correctly typed. The compiler does not check what the declaration means. The authors of "Beyond Compilation" measured how much the "it compiled" metric overstates the quality of autoformalization, that is, translating mathematical statements from natural language into Lean. The headline number: an agent with tools compiles 87.2% of 227 university-level statements, but the semantic criterion accepts only 57.7%. The gap of 29.5 percentage points is Lean code that looks flawless and states something other than what was asked.

How the check works

Most tasks have no reference Lean translation, so there is no "gold" answer to compare against. The authors introduce a composite criterion: a statement is accepted if it compiles in Lean and two LLMs from different model families independently judge it a faithful translation of the original wording.

The criterion was tested in an independent random audit. It matched the majority of human annotators in 91.5% of cases. Its errors are asymmetric: it rarely lets a wrong translation through, but it rejects some correct ones. In other words, the estimate is conservative and tends to understate system performance.

Main results across the eight systems:

• the gap between the share of compiled and accepted statements ranges from 1.3 to 29.5 percentage points;
• the tool-using agent: 87.2% compiled versus 57.7% accepted;
• humans reviewed all of the agent's rejections: 23.8 of the 29.5 percentage points turned out to be real translation errors;
• for six of the seven one-shot systems, 78–100% of the gap consists of genuine translation errors, according to a two-stage review by Claude Opus 5.5 with Lean and GPT-6.1 Sol, checked against human annotation.

When the judge is wrong

The most unexpected part concerns newer models. GPT-5.2 served as one of the two judges. The authors had it evaluate translations from two later models, GPT-6 Astra and Claude Opus 5.5. The judge accepted 83% of statements from each. GPT-5.2's own one-shot result was 21%.

The two-stage review then examined the rejections of those two models. Of 54 rejected statements, only 4, or 7%, were real translation errors. The rest were judge mistakes. This fits simple logic: the less often a system errs, the fewer genuine errors there are among its rejections, and the more the judge's own noise stands out. A judge that does not improve alongside the models it evaluates becomes the bottleneck of the benchmark.

For the industry, the takeaway is uncomfortable. An LLM-judge metric is nearly honest for weak systems, but for strong ones it starts to understate quality. You cannot use it to compare models from different generations without re-checking the rejections.

What the tool ablation showed

The authors ran the agent through a 2^3 ablation, switching three tools on and off across all eight combinations. Most of the compilation gain comes from Lean feedback: the agent sees errors and fixes its code. But almost half of that gain fails the semantic criterion. The agent learns to get code to compile, not to get the meaning right. A typical pattern: to clear an error, the statement drops a condition, weakens a quantifier, or has its structure swapped out.

What to change in practice

If you are building an autoformalization pipeline or training a model on a signal from Lean, compilation as the sole reward gives a biased estimate and pushes the model toward degenerate formulations. You need at least one semantic layer: judges from different model families and spot-check human review of rejections.

When working with newer models, check whether the judge is falling behind the system it evaluates. If most rejections turn out to be judge errors rather than translation errors, it is time to revisit the metric. The code and data are published on GitHub (grenadeComing/beyond-compilation), so you can reproduce the approach on your own statements.