In interactive proof assistants such as Lean, a generated proof must pass machine compilation checks, eliminating the need for human scoring. Direct generation fails on multi‑step numeric propositions because the overall pass rate follows a $k$‑th power law of the per‑integer accuracy. A controlled corruption experiment on 2,617 reference proofs confirmed this power‑law behavior.
SCOPE (State‑Conditioned Operator Planning and Execution) overcomes this limitation by a natural division of labor: the language model plans over an operator vocabulary, a symbolic engine executes the numerics, and a compiler renders the final proof. On a 218‑problem benchmark, a 135M‑parameter backbone certifies 191 problems (87.6%). In contrast, the 7B DeepSeek‑Prover‑V1.5‑RL certifies only 18 problems despite consuming 27.5× more tokens and 37.5× more wall‑clock time, and DeepSeek‑Prover‑V2‑7B certifies none on a bidirectional dual suite.
Multi‑step reasoning costs on average 6.12 discrete decision actions per problem and produces no natural‑language thinking text. Replacing the lagged engine state in the decision frame with the current state lifts the pass rate from 117/218 to 191/218, while up‑weighting the chain‑end loss degrades performance.
On the public Lean‑Workbook library, 2,132 of 3,536 gradeable admissible problems certify (60.29%) with zero regression on the main suite. All readings stem from a version‑frozen review with independent rechecks and reverse verification.
Restricting free generation and keeping decision‑time information visible proves a more direct route than simply scaling the model.
Review