Most of a Formal Proof is Forced

A language model that writes mathematics can produce something that looks like a proof and is not one. We grade against the Lean 4 lambda calculus kernel: a candidate is accepted when its inferred type matches the stated goal, using a binary metric that cannot be hallucinated. On this surface, the next token is largely forced by the goal type and elaboration context, with the residual entropy concentrated at a sparse set of genuine decision points. A from-scratch and transferred scaling sweep reads loss exponents three to four times steeper than the natural-language reference on both data and parameter axes, with a small irreducible floor; the exponents are calibration-invariant to the tokenisation scheme. For models larger than 30M, model size becomes redundant, and loss is set by effective data alone. The concentrated entropy makes depth-first search cheap: one model call per emitted step boundary, free chain rollout between them. We demonstrate nontrivial empirical performance with supervised fine-tuning alone, paving the way for a potentially competitive prover.