Paper deep dive
SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner
Hanchao Zhou, Jialei Li
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:In proof assistants such as Lean, a generated proof must pass machine compilation checks, so evaluation needs no human scoring. Direct generation fails on multi-step numeric propositions: a proof is valid only if every content integer is correct, so the pass rate is bounded by the k-th power of the per-integer accuracy. Controlled corruption across 2,617 reference proofs confirms this power law. SCOPE (State-Conditioned Operator Planning and Execution) enforces the natural division of labor: the model plans over an operator vocabulary, a symbolic engine executes the numerics, and a compiler renders the proof. On a 218-problem suite it certifies 191/218 (87.6%) with a 135M backbone; the 7B DeepSeek-Prover-V1.5-RL certifies 18/218 at 27.5 times the tokens and 37.5 times the wall-clock, and DeepSeek-Prover-V2-7B certifies zero on a bidirectional dual suite. Multi-step thinking costs 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 one lifts the pass rate from 117/218 to 191/218, while up-weighting the chain-end loss hurts. 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 come from a version-frozen review with independent rechecks and reverse verification. Restricting free generation and keeping decision-time information visible is a more direct route than enlarging the model.
Tags
Links
- Source: https://arxiv.org/abs/2610.08319v1
- Canonical: https://arxiv.org/abs/2610.08319v1
Trouble viewing inline? Open PDF directly →
Full Text
100,884 characters extracted from source content.
Expand or collapse full text
SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner Hanchao Zhou Jialei Li †thanks: Jialei Li (e-mail: gayly0414@163.com). Corresponding author: Hanchao Zhou (e-mail: zhouhanchao6@gmail.com). Abstract In proof assistants such as Lean, a generated proof must pass machine compilation checks, so evaluation needs no human scoring. Direct generation fails on multi-step numeric propositions: a proof is valid only if every content integer is correct, so the pass rate is bounded by the k-th power of the per-integer accuracy. Controlled corruption across 2,617 reference proofs confirms this power law. SCOPE (State-Conditioned Operator Planning and Execution) enforces the natural division of labor: the model plans over an operator vocabulary, a symbolic engine executes the numerics, and a compiler renders the proof. On a 218-problem suite it certifies 191/218 (87.6%) with a 135M backbone; the 7B DeepSeek-Prover-V1.5-RL certifies 18/218 at 27.5 times the tokens and 37.5 times the wall-clock, and DeepSeek-Prover-V2-7B certifies zero on a bidirectional dual suite. Multi-step thinking costs 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 one lifts the pass rate from 117/218 to 191/218, while up-weighting the chain-end loss hurts. 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 come from a version-frozen review with independent rechecks and reverse verification. Restricting free generation and keeping decision-time information visible is a more direct route than enlarging the model. Index Terms: Automated theorem proving, formal verification, large language models, Lean, neuro-symbolic systems. I Introduction Automatic generation of formal proofs has long been a hard problem at the intersection of artificial intelligence and formal verification. Proof assistants such as Lean [1] bring propositions, proofs, and the checking process into one machine-verifiable framework: a candidate proof is accepted only if the compiler confirms that every step is legal and that no unproven assumption is used. This property makes theorem proving a suitable testbed for studying the reasoning ability of language models: evaluation involves no human scoring, and surface fluency earns no credit. In recent years, language models ranging from hundreds of millions to tens of billions of parameters have made a series of advances in this direction, yet certified pass rates on propositions that require multi-step numeric derivation remain low. Failed samples show a consistent pattern: the proof is structurally conventional (it uses standard tactics such as induction, rewriting, and normalization) but breaks at concrete numeric values and ends with an unsolved goal (sorry in Lean). The pattern suggests that the bottleneck may lie not in the choice of proof steps but in generating the numeric content one item at a time. The division of labor can be stated quantitatively: the validity of a long proof is the conjunction of all its numeric content. If the model writes each content element correctly with probability p and a proof contains k elements, the pass rate of direct generation is bounded above by pkp^k. When k grows with problem difficulty, any fixed p below one drives the pass rate down exponentially. Our experiments support this analysis and fold the countermeasure into the same architectural frame: if the analysis holds, the rational architectural response is to narrow the model’s role to policy planning free of numeric generation, hand numeric computation to a symbolic tool, and hand proof text to template compilation. In human mathematical practice, the core competence of solving lies to a large extent in perceiving and choosing tools: judging which theorem, which lemma, which transformation, or which algorithm applies to the proposition at hand. Carrying out the computation is comparatively mechanical and has always been done precisely by external procedures. We therefore test a division-of-labor hypothesis: let the language model supply the connection between problem and tool, and let a symbolic computing component execute the numerics; then examine whether this division supports long-chain, multi-step, exact reasoning. Specifically, on three families of constructively generated discrete-mathematics problems (induction, inequalities, and number theory), we build a complete system called SCOPE (State-Conditioned Operator Planning and Execution). The backbone is the 135M-parameter SmolLM2 [2], fitted with an operator-selection head and an argument-prediction head that produce a solution chain step by step inside a vocabulary of 194 operators; the numerics of each step are computed by a symbolic execution engine that returns the state; the proof text is generated by a compiler from the chain and the engine’s results, and is finally reviewed by the Lean compiler. On this architecture we run a set of experiments that isolate one variable at a time, plus an external-model comparison. The main results follow. When complete proof text is generated directly, token-level accuracy and certified pass rate diverge sharply: the model’s token accuracy on a held-out set from the training distribution is 0.9637, yet certified passes on the 218-problem suite number 0/218; a same-distribution control set (20 problems) yields one pass, matching the power-law prediction of about 0.031 computed from the number of content elements per proof (about 14.9). The 7B DeepSeek-Prover-V1.5-RL [3] passes 18/218 on the same suite, with 177 outputs terminating in sorry, the same pattern. Once proof text is produced by the compiler instead, the pass rate of the same model on the same suite rises from 1/218 to 117/218. The compiler reproduces the reference proofs byte for byte on all 2,399 corpus rows and certifies 218/218 when fed the reference chains of the test suite, so this stage contributes no precision loss. Analysis of the remaining errors further localizes the failure to the final step of the chain: all 101 first errors among the 101 errors occur at the last step. The residual class read off the final step stands in a fully determined correspondence with the engine’s residual value (799/799 on the corpus and 181/181 on the test suite), but the decision frame carries a state that lags one step behind. A 2×22× 2 factorial experiment (state shifted or not, crossed with chain-end loss weight) shows: shifting the state raises the pass rate from 117/218 to 191/218; up-weighting the loss lowers it (117 to 110; with the state shifted, 191 to 172). In resource terms, this architecture emits 6.12 decision actions per problem on average, takes 0.53 s per problem, and peaks at 833 MiB of inference memory; the comparison model emits 168.0 generated tokens, takes 19.88 s, and peaks at 8,567 MiB. The two systems differ in interface conditions: the comparison model has no execution engine or compiler and must generate the complete proof as free text. We use this comparison as evidence on the structure of the output channel. The contributions of this paper are as follows. We give, in a controllable domain, the error-product structure of direct long-proof generation and verify it quantitatively. We propose and implement SCOPE, an architecture in which the language model serves as the policy planner, a symbolic engine serves as the computing component, and a compiler serves as the text-generation component, reaching an 87.6% certified pass rate on the test suite. The model’s multi-step thinking is endogenous to the architecture and enabled by default: it happens in the latent decision space over operator chains, produces no natural-language thinking text, and costs 6.12 decision actions per problem on average. Thinking never passes through the output channel, yet the system is not a black box: per-step decision distributions and engine states can be read out directly. A factorial experiment attributes the main information bottleneck of chain decisions to state visibility at decision time rather than to loss allocation. For all readings we establish a validity pipeline of version-frozen review plus independent recheck plus reverse verification. We complete a domain-extension validation on a public problem library: the admissible domain is determined by mechanical checks and disclosed layer by layer, model-independent readings are reported separately from system readings, and an independent final audit verifies the numbers. Code, corpus, and review programs will be released. I Related Work The use of language models for theorem proving has evolved from tactic-level prediction to complete proof generation. GPT-f [4] and follow-up work train tactic-prediction models in the Lean and Metamath environments; ReProver [5] and related retrieval-augmented methods improve proof search with premise selection; the DeepSeek-Prover line [6], [3] trains proof-specialized models on Lean 4 from large-scale synthetic data, with proof-assistant feedback reinforcement learning entering at V1.5 and evaluation centered on benchmarks such as miniF2F [7] and Lean-Workbook [8]; its V1.5 release is the comparison model of this paper. The common form of these methods is what we call the direct-generation paradigm: the model produces proof text or tactic sequences itself. Its failure mode on multi-step numeric propositions is the subject of our first empirical law. Open environments such as LeanDojo [5] provide the evaluation infrastructure for this line of work. Another line couples learning with symbolic search: HyperTree Proof Search [9] explores proof trees under a transformer guide, Magnushammer [10] replaces hand-tuned premise selection with a learned retriever, Draft-Sketch-Prove [11] turns an informal draft into a formal sketch that smaller provers complete, AlphaGeometry [12] pairs a language model with a symbolic deduction engine, and AlphaProof [13] carries the recipe to competition-level problems. Assistant-style tools bring models inside proof assistants: Baldur [14] generates and repairs whole Isabelle proofs from failure feedback, and Lean Copilot [15] serves tactic suggestions natively in Lean 4; in both, the model remains in the role of producing proof text. Learned neuro-symbolic models of this broad family are an established design space in this journal [16]. What the proof-producing systems above do not provide is a controlled analysis of the failure mechanism that concerns us here, the conjunction structure of long numeric derivations. Research on tool-augmented language models shows that delegating numeric computation or code execution to external tools improves reliability on the corresponding tasks; representative work includes program-aided language modeling [17] and code-interpreter invocation [18], and documented failures of language models on fine-grained character- and symbol-level manipulation [19] sharpen the case for delegation. The difference here is that tool calls are not wholesale delegation (generate a program once, then run it) but are embedded in the step-by-step decision process, with every decision conditioned on the state the tool returns; the tool state itself enters training and inference as model input, and we examine the link between state visibility and decision correctness on that basis. Curriculum learning [20] and constructive data synthesis are widely used in mathematical-reasoning training; the distinctive property of our corpus engineering is auditability: every training row carries an executable reference chain and has passed a mechanically executed leakage check. Work related to our error analysis includes exposure bias and its remedies in sequence generation [21], [22], error compounding that deepens with derivation length in compositional tasks [23], and step-level verification of reasoning chains [24], with chain-of-thought prompting [25] as the common substrate. Most of these works observe the phenomenon indirectly, through end-to-end metrics on natural-language reasoning tasks; we reduce it, in a certified setting, to a computable structure, namely a Boolean conjunction of proof validity over content elements, which yields a definite power-law relation between pass rate and per-element accuracy and admits direct examination under controlled conditions. I Method This section describes the components of SCOPE. The system takes a mathematical proposition written in a domain-specific language as input and outputs a proof certified by the Lean compiler. Processing has four parts: the discrete representation of propositions and the operator vocabulary (Section I-A), the symbolic execution engine (Section I-B), the chain-planning model (Section I-C), and the proof compiler (Section I-D); the review protocol is given in Section I-E. Fig. 1: The SCOPE architecture and data flow. A mathematical proposition enters a latent decision loop through discrete encoding: the chain planner, with its operator and argument heads, handles perception and routing and commits to one decision per step inside the operator vocabulary, which supplies both operator semantics and rendering templates; the symbolic engine executes each step exactly, and the state frame, after the state shift, feeds back into the decision loop, so multi-step thinking is carried endogenously by the loop with zero generated tokens (the Zero-token thinking label in the figure). The chain and its arguments go to the proof compiler, which renders Lean text from the templates; the Lean compiler reviews it, a frozen review program performs an independent recheck and reverse verification, and a certified proof is output. I-A Task Definition and Operator Vocabulary The problem domain covers three families of elementary discrete mathematics: induction identities, polynomial inequalities, and elementary number-theoretic divisibility. Each proposition is produced constructively by a parameterized generator together with a reference solution chain and a reference proof; generation guarantees solvability, and the reference solution is verifiable by mechanical execution. A proposition is given as a state: the objects it mentions (variables, polynomial coefficients, moduli) appear as a fixed field structure rather than as natural language. Solving is modeled as an operator chain, where each step consists of an operator identifier and a list of concrete arguments, and the chain ends with an explicit terminator. All legal operators form a finite vocabulary; the initial release contains 194 operators, extended to 220 for the public library (Section X). The vocabulary grows in successive batches: each new batch of operator rows receives only incremental training, with zero regression on existing capability as the acceptance gate. Every operator has an executable semantics in the engine. The vocabulary is organized by problem family, for example the nested-induction family, the multi-lemma-combination family, and the sum-of-squares decomposition family; operators of one family share argument structure and state-update form. The model never touches Lean tactic names; the correspondence at tactic level is handled by the compiler. For later reference, we fix the formal notation as follows. Definition 1 (problem state): a problem state is an integer vector with a fixed field structure, s=(x1,…,xd)∈ℤds=(x_1,…,x_d) ^d (1) where the fields correspond to the objects of the proposition (variables, polynomial coefficients, moduli), and one problem-type family shares one field structure. Definition 2 (operators and solution chains): the legal operators form a finite vocabulary O (194 initially, 220 after the public-library extension); each operator o∈Oo∈ O carries an argument vector a of operator-specific shape; one decision is the pair (o, a). A solution chain is a finite sequence τ=((o1,a1),…,(oT,aT))τ= ((o_1,a_1),…,(o_T,a_T) ) (2) where T is the chain length, and the chain terminates with an end symbol. Definition 3 (execution engine and certification): the execution engine is a deterministic map E:(s,o,a)↦(s′,cert)E:(s,o,a) (s ,cert) that returns a unique state s′s and an execution certificate cert for identical inputs. Write acc(π)=1acc(π)=1 if proof text π passes certification, i.e., it compiles in Lean and the compiled result depends on no unproven assumption; every certified pass rate reported in this paper is the mean of acc over the corresponding problem set. Definitions 1 to 3 fix the formal objects of the system, and the solving goal can now be stated: given a problem state s, find a solution chain whose compiled proof passes certification, i.e., find τ such that acc(C(τ,s))=1find τ such that acc (C(τ,s) )=1 (3) where C is the proof compiler (Section I-D, formalized in (12)) and acc is the certification indicator of Definition 3. This search cannot be carried out by enumerating chains: the number of candidate combinations per step is the product of the vocabulary size and the value-space size (220 and 352 in our configuration), chains run 5 to 9 steps, and the chain space exceeds the fifth power of that product. The role of the chain-planning model (Section I-C) is to locate the correct chain in this space, step by step, under a learned conditional distribution. Table I maps the problem-domain layers onto the composition of the vocabulary. The vocabulary grows in batches, each covering a problem type or one domain extension; every batch has executable semantics in the engine (Section I-B), and the vocabulary carries a per-operator admissibility matrix over multiplier rows that restricts the legal argument set of each decision. TABLE I: Problem-domain layers and the composition of the operator vocabulary. The initial release has 194 rows (first four segments) and the public-library extension raises the count to 220 (Section X); per-segment counts are measured from the system’s vocabulary registry. Vocabulary segment Rows Covered problem types and introduction batch Base segment 161 Core operators and skeleton rows of the initial three domains (induction identities, polynomial inequalities, number-theoretic divisibility) Deep-chain extension segment 17 Closed-form operators of the deep-chain corpus: sum-of-squares closed forms, geometric and summation closed forms, block closing, partial fractions, and high-tower combinations Construction-curriculum segment 7 Three construction curricula: induction recursion, ring identities, sum-of-squares decomposition, divisibility witnesses Deep-chain family segment 9 Nested-induction chain construction (difference-equation solving, folding, telescoping check, closed-form closing) and sum-of-squares chain construction (single-variable blocks, cross blocks, three closing types) Substitution and evaluation segment 4 Algebraic evaluation, modular evaluation, and variable substitution Routing segment 9 Route operators from public-library problem statements to existing families Extension segment 13 Nine extension families: goal-shape splitting, quantifier introduction, existence witnesses, predicate unfolding, radical reduction, symbolic exponentiation, factorials, library-name entry, and chained relations Total 220 — I-B Symbolic Execution Engine The execution engine is a set of deterministic symbolic-computation programs, one execution function per operator. Given the current state and the arguments, the function performs the computation and returns two things: the numeric intermediate result, and a mechanically checkable execution certificate (for example, an algebraic identity check that passed). Taking the sum-of-squares decomposition family as an example, each step removes one square component from the goal expression and returns what remains, which we call the residual; its update rule is Rout=Rin−mℓ2R_out=R_in-m\, ^2 (4) where RinR_in and RoutR_out are the residuals before and after the step, m is the coefficient of the removed square term, and ℓ is the corresponding linear form. The residual enters the model’s state frame as an eight-dimensional numeric vector (Section I-C). All engine computation uses exact integer and rational arithmetic and contains no floating-point error; the engine is implemented in C++/CUDA, is bit-aligned with the training-side reference implementation, and runs more than five times faster than it. The final step of a chain must classify the final residual ρ:ρ: c(ρ) c(ρ) =0(ρ=0);c(ρ)=square(ρ∈4,9,16,25,36,49); =0\ (ρ=0); c(ρ)=square\ (ρ∈\4,9,16,25,36,49\); (5) c(ρ) c(ρ) =other(otherwise) =other\ (otherwise) This correspondence holds for every problem in the corpus and the test suite (799/799 and 181/181) and underlies the factorial analysis of Section VIII. Two design constraints govern the engine-model interface. First, the arguments fed to the engine take reference values during training and model predictions at inference; if a predicted argument is illegal (for example, outside its domain), the engine rejects execution and the step is scored as an error. Second, the engine returns a fixed-dimensional state for every operator, so the states of different operators can be concatenated within one frame structure. For the mainstay operator of the sum-of-squares family (single-variable block absorption), executing (4) inside the engine must satisfy an exact absorption criterion: one square component is removed if and only if the residual decomposes into that square term and a remainder that contains no nonzero term in any variable supporting the removed linear form, i.e., Rin R_in =mℓ2+Rout, =m\, ^2+R_out, (6) and the coefficients of the variables the coefficients of the variables of ℓ in Rout are all zero in R_out are all zero The two conditions together make the removal exact; arguments that fail the criterion (for instance m not a positive integer, or a remainder that still contains terms in variables supporting OPENℓ) ) are rejected by the engine. The criterion is verified mechanically on a finite test grid: Rin(k) R_in(k) =mℓ(k)2+Rout(k), =m\, (k)^2+R_out(k), (7) for all k on the verification grid all k on the verification grid The grid is determined by the variable domains and a degree bound; passing the verification issues the execution certificate of the step, which is written to disk together with the chain (Section I-G). Table I lists representative operators of each problem family and their execution logic. Operator names are the identifiers of the implementation (family-prefixed in the released code); for each family we show one or two operators that carry its main computation; full specifications of all operators ship with the code. I-C Chain-Planning Model The planning model uses SmolLM2-135M [2], a transformer decoder [26], as the backbone and adds two output heads: the operator-selection head gives, over the vocabulary, the distribution of the next operator, and the argument-prediction head gives that operator’s arguments, predicted in a discretized value space (352 candidates). Writing the problem state as s and the representation of the executed steps as h1,…,ht−1h_1,…,h_t-1, the decision at step t is TABLE I: EXECUTION LOGIC OF REPRESENTATIVE OPERATORS. THE EXECUTION SEMANTICS AND CERTIFICATES ARE THE ACTUAL CHECKING PROCEDURES INSIDE THE ENGINE; THE RENDERED TACTICS ARE THE LEAN TACTICS THE COMPILER EXPANDS FOR THAT STEP. Operator (family) Execution semantics Execution certificate Rendered tactics sos_block (sum-of-squares) Deducts one single-variable square component from the current residual per (4) Grid identity (7) plus absorption criterion (6); m a positive integer positivity sos_tail_other (sum-of-squares) Classifies the final residual per (5) and closes the chain Closed-chain identity: the goal equals the sum of deducted squares plus the final residual norm_num, nlinarith only nest_solve (nested induction) Solves one difference equation from increment and initial value, yielding a polynomial closed form Quadruple check: exact degree, initial value, telescoping grid, degree ladder rw and ring inside induction nest_delta (nested induction) Verifies that the closed form satisfies F(k+1)−F(k)=S(k)F(k+1)-F(k)=S(k) Pointwise identity of the forward-difference grid Certificate-level check; emits no tactic lines s_poly (routing) Recognizes the statement as a polynomial identity and invokes ring-law verification Ring-law recomputation ring s_eval (routing) Recognizes the statement as numeric evaluation and computes step by step Exact arithmetic recomputation norm_num sqrt_iso (extension families) Gives exact values for radicals of perfect-square closed forms; squares one-sided radical inequalities under side conditions Grid check of side conditions rw (radical equivalence theorems) intro_binder (extension families) Strips the leading universally quantified binder and passes the body to existing routes Structural check intro (ot,at)=fθ(s,h1,…,ht−1)(o_t,a_t)=f_θ(s,h_1,…,h_t-1) (8) where ot is the operator choice, at the arguments, and θ the model parameters. Decisions proceed autoregressively until the model emits the terminator or the step budget is reached. The two output heads expand fθf_θ into discrete distributions. Write the decision frame as Ft=(s,h1,…,ht−1)F_t=(s,h_1,…,h_t-1) (consistent with Algorithm 2); the operator head gives a distribution over the vocabulary O, and the argument head a distribution over the value space V with |V|=352|V|=352: P(ot=o∣Ft) P(o_t=o F_t) ∝exp(zo(o)), (z_o(o) ), (9) P(at=v∣ot,Ft) P(a_t=v o_t,F_t) ∝exp(za(v)) (z_a(v) ) where zoz_o and zaz_a are the logits of the two heads on the decision frame, and the legal value set of each operator is restricted by the admissibility matrix carried with the vocabulary (Table I). At inference, the highest-probability item is taken at every step. The training objective is the cross-entropy of operator selection and argument prediction, supervised by the reference chain (ot∗,at∗)(o_t^*,a_t^*): ℒ=ℒop(ot,ot∗)+124ℒval(at,at∗)L=L_op(o_t,o_t^*)+ 124\,L_val(a_t,a_t^*) (10) where the argument term is scaled by the total number of value slots (24). The chain-end weighting configuration gives the operator cross-entropy at the terminating step (t=Tt=T) an extra weight, bringing its total weight to λ(CLOSEλ(Experiment 4 uses λ=5λ=5): ℒW=ℒ+(λ−1) 1[t=T]ℒopL_W=L+(λ-1)\,1[t=T]\,L_op (11) All experiments share one training configuration: 6,000 steps, batch size 6, learning rate 4×10−5× 10^-5, random seed 20260923, and the same batch-order file (whose checksum is identical across configurations), so that any difference between configurations is attributable to a single variable. The training dynamics of the final configuration (loss components and gradient norms over the 6,000 steps) appear in Fig. A1. An earlier version of the model also carried a proof-text generation head (used in Experiments 1 and 2 of Section VI); it was removed following the findings of Section VII. Algorithm 1 Training the chain-planning model 0: deep-chain corpus D (with reference chains (o∗,a∗)(o^*,a^*) and per-step ground-truth engine states); batch-order file; 6000 training steps; batch size 6; learning rate 4×10−54× 10^-5. Convention: during training, the state and arguments in the decision frame take reference values (Section I-B). 1: initialize parameters θ (SmolLM2-135M backbone plus operator-selection and argument-prediction heads) 2: for step =1=1 to 60006000 do 3: draw a mini-batch (s,o∗,a∗)⊂D\(s,o^*,a^*)\⊂ D following the batch-order file 4: for each sample, read the decision frame step by step (19); compute (ot,at)←fθ(⋅)(o_t,a_t)← f_θ(·) 5: L←Lop(ot,ot∗)+(1/24)Lval(at,at∗)L← L_op(o_t,o_t^*)+(1/24)\,L_val(a_t,a_t^*) (10) 6: if end-step weighting enabled (Exp. 4B/C, λ=5λ=5): L←L+(λ−1) 1[t=T]LopL← L+(λ-1)\,1[t=T]\,L_op (11) 7: θ←update(θ,∇L)θ (θ,∇ L) 8: end for 8: trained parameters θ and the training log (steps, losses, and checksums). I-D Proof Compiler Proof text is produced by a compiler: given an operator chain, the compiler expands each step into Lean tactic sequences under the operator’s template rules, and every number in the output comes from the engine’s actual computation. The compiler calls no language model and reads no reference proof text. Its correctness rests on two verifications: on all 2,399 corpus rows, the compiled output matches the reference proof byte for byte (2,399/2,399); on the test suite, feeding the reference chains yields proofs that all certify (218/218). Consequently, whenever the model’s chain is correct, the compiled proof certifies, and the certified pass rate of the system is determined entirely by the quality of chain decisions. Compilation is a deterministic map. Writing E(τ, s) for the step-by-step execution results (the state and certificate sequence) of chain τ started from state s, the proof text is π=C(τ,E(τ,s))π=C (τ,E(τ,s) ) (12) The map C has no free parameters and calls no language model: template rules fix the tactic skeleton, and all numbers come from the actual computation in E(τ, s). Since C reproduces the reference proofs byte for byte on the corpus (2,399/2,399), the search problem of (3) reduces entirely to the chain-decision problem. Algorithm 2 SCOPE solving one problem 0: problem state s; operator vocabulary O; execution engine E; proof compiler C; step budget TmaxT_ . 1: h←∅h← ; t←1t← 1 2: while t≤Tmaxt≤ T_ do 3: read decision frame Ft=(s,h1,…,ht−1,Rout(t−1))F_t=(s,h_1,…,h_t-1,R_out^(t-1)) (19) 4: (ot,at)←fθ(Ft)(o_t,a_t)← f_θ(F_t) (8) 5: if oto_t is the terminator then break 6: (s,cert)←E(s,ot,at)(s,cert)← E(s,o_t,a_t); ht←(ot,at)h_t←(o_t,a_t) (4) 7: t←t+1t← t+1 8: end while 9: τ←(h1,…,ht−1)τ←(h_1,…,h_t-1); π←C(τ)π← C(τ) 9: the operator chain τ, the proof text π, and per-step records (decision distributions, arguments, engine states, and certificates). I-E Review Protocol Review is performed by an independent automatic program: a candidate proof is compiled in the Lean environment, and the compiled result is checked to depend on no unproven assumption (no sorry and no corresponding axioms). The program stayed version-frozen for the entire experimental period (anchored by an MD5 checksum, given in Appendix B), and every experiment was checksummed once before and once after review. To rule out bias introduced by review itself, a dual-protocol recheck is executed: at least 60 accepted proofs, drawn in strata, are re-reviewed one by one through an independent path; in the reverse direction, 12 corrupted proofs of each of two kinds (final segments truncated; proofs of other problems substituted) are submitted, and the program is required to reject them. Across all experiments the two protocols show zero discrepancies, and reverse verification rejects all cases. I-F Auditability The design makes the entire solving process inspectable step by step. The model’s output is not free text but an operator chain inside a restricted vocabulary: each step consists of an operator identifier and concrete arguments, whose legality can be checked one item at a time against the engine’s semantics. This property forms the contrast with the direct-generation paradigm: the intermediate steps of a free-text proof admit no mechanical inspection, and evaluation must rely on the final compilation result. In this architecture, any output can be replayed as a complete decision sequence, and an error can be pinned to a specific step. Auditability at the computing layer comes from the determinism of the engine. The engine executes every step in exact integer and rational arithmetic and returns the numeric state plus a mechanically checkable execution certificate; for example, the correspondence between the final class and the residual value holds row by row on the corpus and the test suite (799/799 and 181/181), so the correctness of this stage can be verified independently of the model. Proof text is generated by the compiler from templates; it matches the reference proofs byte for byte on all 2,399 corpus rows and certifies on all 218 test problems given the reference chains, showing that the text stage contains no free parameters. Auditability at the review layer rests on three mechanisms: the review program is version-frozen (MD5-anchored, checked before and after grading in every experiment); accepted samples are re-reviewed through an independent path in strata (66/66 zero discrepancies, replicated across two configurations); reverse verification rejects all corrupted proofs (12/12 for both truncation and substitution). Two zero-capability controls (the untuned backbone and a rule-based solver, 1,080 applicable problems each with zero passes) further rule out earning certified scores by guessing or pattern matching. Auditability at the experiment layer takes the form of configuration control and record completeness: all configurations share the batch-order file (identical checksums) and random seeds; the differing variable of each configuration is registered in the design file in advance; every results file carries a checksum ledger. A direct payoff of auditability is error analysis at decision-step granularity: the 101 first errors of Section VIII all localize to the final step of the chain, which presupposes the symbolic decision sequence; attribution at this granularity cannot be obtained directly from free-text output. I-G Process Auditability and Observability of Latent Thinking The intermediate process consists of explicit symbolic structures and can be inspected item by item. For every problem, the system writes to disk: the model’s complete operator chain, the arguments of every step, the residual and execution certificate returned by the engine, the proof text produced by the compiler, and the review program’s verdict with its reason (the compilation result and the axiom dependencies). Errors can therefore be pinned to specific steps: Section VIII localizes all 101 errors to the final step of the chain and reports the predicted probability at each erroneous step (55 of them at 0.9 or above). Step-level analysis of this kind lacks an operational counterpart in the free-text generation paradigm: text output offers only an aggregate right-or-wrong signal and surface statistics. In the final configuration of this paper, multi-step thinking is the default behavior granted directly by the training objective; no prompt or mode switch triggers it. The entire solving process consists of step-by-step decisions over the operator chain and produces no natural-language output: on average 6.12 discrete decision actions per problem (Section IX), with the proof text compiled separately. Because the carrier of decision is a discrete symbolic structure, the thinking process is observable from outside, and the observation does not rely on the model’s self-report: the operator-selection distribution, the predicted arguments, and the engine-returned state of every step can be read and tallied directly. The hidden state of the decision frame is equally readable: in low-dimensional projection it organizes by problem family (nearest-neighbor purity 0.999), the frames of one problem advance continuously along the chain (Fig. 2), and the projected vectors are frame-for-frame identical to the hidden states that the output heads actually consume. By comparison, the observability of chain-of-thought comes at the price of generated tokens, and natural language produced as an explanation can disagree with the model’s actual reasons for deciding; what we observe here is the decision itself. Every stage of the system can be re-verified by a third party. The review program is version-frozen and carries a checksum; accepted samples are re-reviewed through an independent path (stratified sampling, zero discrepancies); reverse-constructed corrupted proofs are all rejected (Section I-E); training configurations, batch order, and random seeds are registered together with the checksums of all reading files, so any reading can be recomputed from the released material; proof compilation is deterministic and fully replayable from the operator chain (2,399/2,399 byte-identical on the corpus, Section I-D); the isolation check between corpus and test suite is a two-level mechanical scan whose program ships with the code. Auditability also makes controlled intervention possible. The factorial experiment of Section VIII directly edits the state quantity inside the decision frame and retrains comparison configurations, thereby attributing a 74-problem change in pass rate to a single variable; frame-level intervention of this kind presupposes a structured process. We will release the code, corpus, review programs, and per-problem records (including per-step decision distributions), so that all experimental readings can be re-checked outside the system. Fig. 2: Low-dimensional projection of decision-frame hidden states (218 problems, 1,552 frames, UMAP [27]). The states organize by problem family (nearest-neighbor purity 0.999 against a random baseline of 0.659); frames of the same problem advance along the chain (adjacent-frame cosine similarity 0.607 versus 0.154 for random frame pairs); the projected vectors are frame-for-frame identical to the hidden states consumed by the output heads (maximum deviation 0). Thinking rides on a discrete decision sequence whose internal state can be read out directly, without relying on the model’s self-report. I-H Worked Examples: From Problem State to Certified Proof This section presents the input, the decision chain, and the output of the system on four real problems. Two come from the main suite (the configuration of Section VIII) and two from the public-library final exam (Section X); the chains and proof texts are the system’s actual records on disk, unedited. The sum-of-squares example shows the residual mechanism in full. The problem is the multivariate polynomial inequality v2+2u2+2w2+z2−2yv+y2+2x2+4v−12u−4w−4z−4y−8x+57≥−7v^2+2u^2+2w^2+z^2-2yv+y^2+2x^2+4v-12u-4w-4z-4y-8x+57≥-7. The model’s chain has six steps: cross-block absorption handles the square containing the cross term −2yv-2yv; four single-variable block absorptions remove four square terms in succession; and the closing step classifies the final residual. Table I lists, step by step, the square component removed at each step and the proof line rendered from it. The final residual is 28, of the other class per (5); the closing accordingly emits a constant-nonnegativity proof line and then closes all goals with a nonlinear-arithmetic tactic. The proof was certified by the review program. TABLE I: STEP-BY-STEP COMPUTATION OF A SUM-OF-SQUARES PROBLEM (ACTUAL RECORD ON DISK). EACH STEP REMOVES ONE SQUARE COMPONENT PER (4); EVERY NUMBER IN THE RENDERED LINE COMES FROM ENGINE COMPUTATION; THE CLOSING ROW GIVES THE FINAL RESIDUAL 28 (OTHER CLASS, PER (5)). Step Operator Component removed, mℓ2m\, ^2 per (4) Rendered proof line (engine-computed values) 1 sos_cross (cross block) 1(−v+y−2)21\,(-v+y-2)^2 have h1 : (0:ℚQ) ≤ 1 * (- v + y - 2) 2 := by positivity 2 sos_block 2(w−1)22\,(w-1)^2 have h2 : (0:ℚQ) ≤ 2 * (w - 1) 2 := by positivity 3 sos_block 2(u−3)22\,(u-3)^2 have h3 : (0:ℚQ) ≤ 2 * (u - 3) 2 := by positivity 4 sos_block 1(z−2)21\,(z-2)^2 have h4 : (0:ℚQ) ≤ 1 * (z - 2) 2 := by positivity 5 sos_block 2(x−2)22\,(x-2)^2 have h5 : (0:ℚQ) ≤ 2 * (x - 2) 2 := by positivity 6 sos_tail_other (closing) ρ=28ρ=28 have hrho : (0:ℚQ) ≤ (28:ℚQ) := by norm_num; nlinarith only [h1, h2, h3, h4, h5, hrho] The nested-induction example is a closed-form problem: the proposition is ∀n:ℕ,fn=4−12n+n2+12n3+4n4∀ n:N,\ fn=4-12n+n^2+12n^3+4n^4, with f defined by a difference recurrence. The model’s five-step chain solves the inner difference equation for the inner closed form, folds it into the outer increment, solves the outer difference equation, runs a telescoping check confirming that the closed form matches the increment pointwise (Table I), and closes with the closed form together with its class. The rendered proof is a two-layer induction structure: an induction first establishes the closed form of the inner recurrence, then an induction on the outer goal uses the previous step’s result, and ring normalization finishes the proof. The proof was certified by the review program. The two public-library examples come from the Lean-Workbook final exam. For the algebraic identity x5−y5=(x−y)(x4+x3y+x2y2+xy3+y4)x^5-y^5=(x-y)(x^4+x^3y+x^2y^2+xy^3+y^4), the chain has two steps: a routing reduction into the polynomial route, rendered as the two tactics norm_num1 and ring. For the number-theory evaluation (29×31+37−41)mod4=3(29× 31+37-41) 4=3, the chain has the same two-step shape into the evaluation route, rendered as a single line of norm_num. Both problems certify. Full records of all four examples (per-step decision distributions, engine states, and certificates) ship with the code. IV Experimental Setup IV-A Pre-Control on the Carrier of Latent Thinking A precondition of this architecture concerns the form the carrier of thinking takes inside the latent space: if the intermediate states of multi-step reasoning are passed between the model’s hidden states as continuous vectors, can later steps read them out reliably? Latent-carrier designs of this kind have recently been explored as alternatives to token-level reasoning chains [28], [29]; whether the carrier survives across steps is a property to be tested rather than assumed. A controlled experiment under a unified protocol (same backbone, same number of training steps, two random seeds) answers no for continuous feedback. As Table IV shows, pure hidden-state feedback reaches a readout accuracy of only 0.01 to 0.06 beyond two hops; the continuous-register scheme averages 0.0246 over all depths; value-format discretization manages only 10% to 15%. The only configuration that reads out fully at a depth of 16 hops is key-token discretization combined with curriculum training, which scores 1.0000 at every depth k=1k=1 to 1616 on formal evaluation. Neither ingredient suffices alone: curriculum by itself reads out at roughly zero, and key format alone needs roughly three to four times the training volume to bootstrap. The external-judge reference group (0.973 to 0.984) shows that the discrimination step itself is feasible; the failure lies in the carrier, not the judge. TABLE IV: Carrier comparison for multi-hop readout in latent space (unified protocol: same SmolLM2-135M backbone, same number of training steps, two random seeds; readings are readout accuracy). Carrier configuration Readout accuracy Verdict Pure hidden-state feedback (continuous vectors) 0.01–0.06 beyond two hops (tail mean 0.0223) Failure Value-format discretization (ground-truth keys) 0.10–0.15 Failure Curriculum training (no key format) About 0 Failure Key-token discretization (no curriculum) Slow bootstrap; needs roughly 33–4×4× the training volume Partial Continuous registers Mean 0.0246 over all depths Failure External judge references (markov/gru) 0.973–0.984 Judge feasible; no carrier specificity Key-token discretization + curriculum training 1.0000 at every depth k = 1–16 Full readout at 16 hops The comparison readings of Table IV come from the discretization line of latent chain-of-thought, whose main configuration (v15 in our notation) is decomposed in Table V. That line uses a dynamic multi-hop task as its carrier: given one member of an operator family (orthogonal, permutation, or cyclic matrix families), the model applies it to a latent state step by step and reads out the terminal state after T steps. The depth curriculum of v15 advances as a ladder: the depth measured by the gate probe rises monotonically from 1 to 16, with all fifteen openings falling between training steps 11,000 and 17,500 (Fig. A2), and the opening of the depth gate was independently re-verified. Depth sampling of training episodes stayed shallower than the gate depth throughout this window (the vast majority of episodes remain at T=1T=1), so the ladder curve measures the trajectory of the gate, not the training distribution itself. After the ladder was fully traversed from T=1T=1 to 1616, the discrete decision carrier of all subsequent experiments in this paper was in place; the comparison readings in the table share the unified protocol of Table IV. This set of comparisons establishes the necessary condition behind all subsequent design: multi-step state in latent space must be pinned to discrete symbols (keys in token format) to survive across steps. The operator vocabulary, the engine state frame, and the compiler rendering of Sections I-A to I-D all presuppose it. A bandwidth estimate (about 6 bits per step) together with the measured depth of 16 hops indicates that the carrier does not bottleneck the task depths of this paper. IV-B Training Corpus The training corpus has two layers. The shallow corpus contains 9,366 proposition-proof pairs with chains of one to three steps, covering the early problem families. The deep corpus contains 2,399 proposition-proof rows built by three deep-chain generator families: the nested-induction family (chain length 5), the lemma-tower family (chain length 9), and the sum-of-squares decomposition family (chain length 5 to 7); the overall chain-length distribution is 1,136 rows at 5 steps, 330 at 6, 133 at 7, and 800 at 9, averaging 6.58 steps. The deep-chain corpus is designed so that multi-step planning genuinely occurs during training: the average chain of the early shallow corpus is only about 1.77 steps, too short to support a study of multi-step behavior. All data carry per-step ground-truth engine states (15,791/15,791 steps nonzero) and position annotations of the content integers of reference proofs (100% coverage); the latter serve the error analysis of Section VI. Isolation between corpus and test suites uses a two-level check: identifier level (exact matching of problem names and statement text, required to yield zero hits) and semantic level (an identity check after algebraic normalization, plus a statement-text four-gram overlap check; rows with overlap of 0.9 or above are removed from the training set). This procedure once detected content-level overlaps when several corpus versions were merged and removed them all; the final training set and test sets share zero problems. IV-C Test Suite The deep-chain test suite is produced from the generator candidate pool by a triple screen: unsolvable by the rule-based solver working from the statement text (so pattern matching cannot answer it), in possession of a reference proof, and passing the overlap check against the training corpus. Of 338 candidates, 218 survive overlap filtering (the four text-domain overlap counts are 7, 120, 217, and 326 problems; the stricter count was adopted to avoid potential contamination, removing 120 problems): 13 nested-induction problems, 24 lemma-tower problems, and 181 sum-of-squares problems. A shallow-chain suite (1,083 problems, chains of one to three steps) serves for evaluating early configurations and as the baseline reference of this paper. Both zero-capability controls score zero on the shallow suite: the untuned backbone and the rule-based solver each have 1,080 applicable problems and fail all of them (3 inapplicable problems excluded), showing that certified scores cannot be obtained by guessing or pattern matching. TABLE V: Mechanism decomposition of the discretization experiment (v15 configuration). The discretization of keys and values, the feedback channel, and the depth protocol are independent and mutually supporting; the control readings come from arm comparisons under the unified protocol (same source as Table IV). Mechanism component Treatment in v15 Related control readings Task carrier Dynamic multi-hop: one operator family (orthogonal, permutation, or cyclic matrices) acts on the latent state step by step; the terminal state is read out after T steps — Value discretization Codebook quantization: the latent state snaps to the nearest codeword; readout and feedback both use the dequantized codeword Continuous-vector feedback: 0.01–0.06 beyond two hops Key discretization Keys represented in token-vocabulary format Values discretized without keys: 0.10–0.15 Depth protocol Curriculum ladder: training depth T rises stepwise from 1 to 16, advancing after each level passes the readout gate Key format without curriculum: roughly 33–4×4× the training volume Depth outcome Ladder fully traversed from T=1T=1 to 1616; gate openings independently re-verified Continuous registers: mean 0.0246 IV-D Configuration Overview The main configurations reported in this paper share the same backbone, training hyperparameters, batch order, and random seed; they differ only in the variables listed in Table VI: how proof text is produced, the chain-end loss weight, and the state timing of the decision frame. Experiments 1 to 3 isolate one factor at a time: Experiment 1 examines direct generation; Experiment 2 adds structured numeric output on top of it; Experiment 3 switches proof text to the compiler. Experiment 4 is a 2×22× 2 factorial design. Experiment 5 is the external-model comparison. IV-E Review Validity The main proportional readings carry Wilson 95% confidence intervals [30], where n is the number of graded problems and z=1.96z=1.96: TABLE VI: Main experimental configurations. Experiments 1 to 4 share the backbone (SmolLM2-135M), training hyperparameters, batch order, and random seed; the four configurations of Experiment 4 differ only in the listed variables. Experiment 5 is an external comparison model and is not subject to these controls. ID Proof-text production Chain-end loss weight Decision-frame state Purpose Exp. 1 Model-generated 1.0 Original (lagged by one step) Direct-generation baseline Exp. 2 Model-generated + value slotting 1.0 Original Isolates the numeric-generation mode Exp. 3 Compiler-generated 1.0 Original Isolates the text-production mode Exp. 4A Compiler-generated 1.0 Original Factorial baseline (same as Exp. 3) Exp. 4B Compiler-generated 5.0 Original Factorial: loss weighting Exp. 4C Compiler-generated 5.0 Shifted to current state Factorial: weighting + state Exp. 4D Compiler-generated 1.0 Shifted to current state Factorial: state (final configuration) Exp. 5 DeepSeek-Prover-V1.5-RL direct generation — — External control CI(p^)=p^+z2/(2n)±zp^(1−p^)/n+z2/(4n2)1+z2/nCI( p)= p+z^2/(2n)± z\, p(1- p)/n+z^2/(4n^2)1+z^2/n (13) The interval is solved from the pivot of a binomial proportion: by the central limit theorem, n(p^−p)/p(1−p) n\,( p-p)/ p(1-p) converges in distribution to the standard normal, and the interval endpoints solve the inequality |p^−p|≤zp(1−p)/n| p-p|≤ z p(1-p)/n. Squaring both sides and rearranging gives the quadratic inequality in p (1+z2/n)p2−2(p^+z2/(2n))p+p^2≤0;(1+z^2/n)\,p^2-2\,( p+z^2/(2n))\,p+ p^2≤ 0; taking the two roots by the quadratic formula, with (p^+z2/(2n))2−(1+z2/n)p^2=z2p^(1−p^)/n+z4/(4n2)( p+z^2/(2n))^2-(1+z^2/n) p^2=z^2 p(1- p)/n+z^4/(4n^2) under the radical, yields the endpoint expression of (13). Beyond the dual-protocol recheck of Section I-E, the following discipline applies to all readings. Every score states the number of graded problems and the total; unexecuted reviews are never counted as zero; stratified recheck samples below the planned size are marked as such. Wherever rendering accuracy serves as the metric, a zero-parameter mode baseline (outputting the most frequent answer in the training set) is reported alongside: on the shallow-chain suite the final configuration reaches 0.9755 against 0.6276 for the baseline, a net gain of 34.8 percentage points, which rules out inflation from templated data. The zero scores of the two zero-capability controls (untuned backbone and rule-based solver), together with reverse verification (all corrupted proofs rejected), show that the review program rejects wrong proofs and passes reference proofs. V Baselines and Negative Results in the Shallow-Chain Era With the curriculum corpus in place, the shallow-chain suite (1,083 problems, chains of one to three steps) produced the first baseline: the formal configuration certifies 180/1083 (16.6%), while the two zero-capability controls, the untuned backbone and the rule-based solver, each have 1,080 applicable problems and score zero, so certified scores cannot come from guessing or pattern matching. Rendering accuracy is 0.9755 against 0.6276 for the zero-parameter mode baseline, a net gain of 34.8 percentage points; inflation from templated data is excluded. The first mechanism-level ablation was run in the same period: adding step-level attention to the chain planner (a first-generation implementation) cost a net 62 problems over the full suite (118/1083 against 180/1083, same suite, seed, and batch order). This negative result points in the same direction as the state-injection ablation of Section IX: the bottleneck does not lie in the expressive power of the decision mechanism. Shallow-chain tasks are solvable, but chains of one to three steps cannot examine multi-step behavior. The deep-chain corpus and the 218-problem deep-chain exam (Section IV-B) then moved the examination ground to a qualitative change; the narrative of the next section starts from the first deep-chain exam. VI Collapse: The Error-Product Structure of Direct Long-Proof Generation The first deep-chain exam, run once the deep-chain corpus and the 218-problem suite were in place, produced the single most consequential reading of this paper. Experiment 1 evaluates direct generation: the model plans the solution chain step by step, and a text-generation head writes the complete proof; certified passes number 0/218. The zero does not come from failed chain decisions: the first-operator hit rate is 218/218 and the exact whole-chain hit rate is 117/218 (53.7%), with the nested-induction family 13/13 and the lemma-tower family 24/24 all correct. Meanwhile, the model’s token accuracy on a held-out set from the training distribution is 0.9637, in sharp contrast to the zero pass rate. Decomposing the generated text identifies the cause of failure. Counting the content integers (coefficients, exponents, constants) of each proof individually: on the training-distribution control set (20 problems), the per-digit accuracy of a single content integer is about 0.79, and each proof carries about 14.9 content integers on average. Writing the content integers of a proof as X1,…,XkX_1,…,X_k, with digit i written correctly with independent probability pi, proof validity requires every digit to be correct: Pass=∏i=1kpiPass= _i=1^kp_i (14) When all digits share the accuracy p, the expression equals pkp^k; taking p as an upper bound on every digit gives the power-law bound: Pass≤pkPass≤ p^k (15) Proposition 1 (product law and power-law bound): suppose a proof contains k content integers, digit i is written correctly with independent probability pi, and certification requires all digits to be correct; then the pass rate is given by (14), and if no digit exceeds accuracy p, the bound of (15) holds. Proof: the certification event is the intersection of the k events that digit i is correct; by independence, its probability is the product of the per-digit probabilities, which is (14). If every digit’s accuracy is at most p, each factor of the product is at most p, so the product is at most pkp^k, which is (15). ■ Corollary (load correction): let S⊆1,…,kS \1,…,k\ be the set of load-bearing integers determined mechanically by the controlled-corruption experiment; changing the value of an integer outside S does not change the certification outcome. The product therefore only needs its factors in S, Pass = ∏i∈Spi _i∈ Sp_i; when all load-bearing digits share the accuracy p, this is (17). Substituting p=0.7919p=0.7919 and k=14.9k=14.9 gives a pass rate of about 0.031, i.e., less than one expected pass in 20 problems; the measured one pass matches the prediction (Fig. 3(a)). On the test suite, the per-digit accuracy of the inequality family is only 0.0911; the same computation puts the pass rate near zero, consistent with the measured 0/181. In other words, the validity of a long proof is the conjunction of all its content elements, and when per-element accuracy is insufficient the pass rate falls exponentially with the element count; token-level metrics do not reflect this structure and therefore do not constitute a valid performance measure in this setting. Enlarging the thinking budget does not help the structure either: in the budget comparison on a synthetic task, doubling the multi-step budget left accuracy flat across levels (about 0.974), showing that the bottleneck is the conjunctive structure of the output channel, not the computational budget. The product structure admits a direct test that does not depend on the model. For the annotated content-integer positions in the reference-proof pool (218 test problems plus 2,399 corpus rows, 2,617 proofs in total), each integer is independently replaced, with probability 1−p1-p, by a random value of the same magnitude (excluding the original value; the sign is kept), and the corrupted proofs are graded by the same review program. The design crosses six values of p from 0.99 to 0.50 with bins of the per-problem content-integer count (bin means 10.4, 15.1, 20.0, and 30.0), for 3,570 sampling runs and 1,680 corrupted units graded (0 review anomalies). The theoretical mean weights the actual sampling structure of the per-problem integer counts and the six values of p: T(p)=1N∑j=1NpkjT(p)= 1N _j=1^Np^k_j (16) The measured pass rate over the full pool is 0.558, slightly above the theoretical value of 0.530, a relative excess of about 5% (Fig. 3(b)). The source of the deviation can be located slot by slot: no corrupted unit at coefficient or exponent positions survives (0/432), and all 1,164 corrupted units of the nested-induction and lemma-tower families are rejected by review; every instance of tolerance occurs at multiplier and linear-form constant positions of the sum-of-squares family. In that family’s proofs the multiplier appears only as a positive scalar, which the nonlinear-arithmetic tactic can absorb, so replacing the number leaves the proof valid (25/25 single-slot corruptions survive; tolerance occurs only at such positions of this family and is a property of the proof template). Accordingly, write S⊆1,…,kS \1,…,k\ for the set of load-bearing integers (determined by the proof template, |S|≤k|S|≤ k); a more precise statement of the pass rate is: Pass≈p|S|Pass≈ p^|S| (17) The controlled-corruption experiment also provides a mechanical way to measure the load-bearing status of each digit position. On this baseline, Experiment 2 changes the numeric output to structured slots: the content-integer positions of the proof template are predicted by the model in a discrete value space instead of being generated freely by the text head, and in one configuration the slot ground truth is supplied by the execution engine. The results: slots with engine supply pass 1/218, slots filled by the model pass 0/218, and the original baseline 0/218. After slotting, the model’s fill-in accuracy reaches 94.5% (39.6% of rows fully correct), yet whole-problem certification stays near zero; the gap between high fill-in accuracy and failure under autoregression comes from the cumulative effect of earlier errors on later conditions in autoregressive generation. The result shows that local improvements in numeric generation (raising per-element accuracy) cannot offset the exponential loss of the conjunctive structure; the free-generation stage itself must be removed. VII Reversal: Compiler-Generated Proof Text The contrast between 53.7% chain navigation and 0/218 certified direct generation pinpoints the text-generation stage. Experiment 3 changes the production of proof text to the compiler (Section I-D); the model outputs only the operator chain, and the text loss leaves the training objective. On the same suite, the certified pass rate rises from 1/218 to 117/218 (53.7%). Moreover, the chains of the existing model (produced by the Experiment 2 configuration), when compiled, certify 121/218, matching the exact hit rate of those chains; the retrained pure-planning model gives 117/218, within four problems of the 121/218 obtained from the existing chains, essentially the same. These readings show that once free-text generation is removed, the certified pass rate of the system is determined entirely by chain-decision quality and the text stage no longer costs anything; the same chain set under the two text-production modes yields 1/218 versus 121/218, which directly quantifies the cost of the free-generation stage. Given that compilation is a deterministic map, verified twice over (byte-identical reproduction on 2,399 corpus rows and 218/218 on reference chains), the certified pass rate of the system equals the correctness rate of the chains the model produces: Pass=P(chain correct),Pass=P(chain correct), (18) Fig. 3: Quantitative tests of Law 1. (a) The pass rate of direct generation decays as a power law in the number k of content integers (p = 0.79), with measured points overlaid (control 1/20, deep-chain suite 0/218, comparison model 18/218). (b) Measured pass rate under controlled integer corruption (0.558) against the independent-assumption theory (0.530), bin by bin. where chain correctness is measured by exact whole-chain match. The equality removes the text stage from the performance variables and leaves chain-decision quality as the only performance variable of the system: the 117/218 of Experiment 3 equals the exact chain hit rate, and the 121/218 of the Experiment 2 chains under compilation matches their hit rate as well. The product structure of Section VI is precisely the form that the right-hand side of this equality takes under the free-text paradigm. VIII Attribution: A Factorial Analysis of Decision-Time State Information Compilation exposes all remaining errors at the final step of the chain. Localizing the 101 errors of Experiment 3 problem by problem and step by step: all 101 first errors occur at the last step of the chain, with no mid-chain errors, no premature termination, and no budget exhaustion; 55 of the erroneous steps carry predicted probability 0.9 or above, i.e., the model is highly confident in its wrong judgments. Combined with (5), the final class is fully determined by the residual value; the residual needed for the verdict is already available after the execution of step T−1T-1, whereas the original decision frame carries the value from before the previous step, a one-step lag. Experiment 4 tests this hypothesis with a 2×22× 2 factorial design: factor one is whether the state frame replaces the lagged value with the current one (the state shift below); factor two is the cross-entropy loss weight at the chain’s final step (1.0 or 5.0). The four configurations are otherwise identical (same batch order, same random seed). Table VII reports the results. Mathematically, the state shift augments the conditioning of (8): (ot,at)=fθ(s,h1,…,ht−1,Rout(t−1))(o_t,a_t)=f_θ (s,h_1,…,h_t-1,R_out^(t-1) ) (19) where Rout(t−1)R_out^(t-1) is the residual after the execution of step t−1t-1 per (4), computed before the decision and placed into the state frame; for the final step, Rout(T−1)R_out^(T-1) is exactly the final residual needed for the verdict. Separating final-step quality from prefix quality yields a two-factor decomposition of the pass rate. Proposition 2 (final-step conditional decomposition): let B be the problem set whose first T−1T-1 steps are all correct, and C the set whose whole chain is correct; then Pass=AT−1⋅qT,Pass=A_T-1· q_T, (20) where AT−1A_T-1 = P(B) is the prefix accuracy and qTq_T = P(C — B) the conditional accuracy of the final step. Proof: a fully correct chain implies a correct prefix, i.e., C⊆BC B, so P(C)=P(B)⋅P(C∣B)P(C)=P(B)· P(C B), which is the claim. ■ On Experiment 3 the decomposition takes concrete values: the 101 first errors all sit at step T, so the prefix accuracy is (117+101)/218=1.000(117+101)/218=1.000 and the conditional final-step accuracy is qTq_T = 117/218 = 0.537; after the state shift it is 191/218=0.876191/218=0.876. The difference between the two configurations, 218×(0.876−0.537)=74218×(0.876-0.537)=74 problems, matches the measurement, so the gain comes from improved conditional quality at the final step; prefix quality is not a loss term in either configuration. TABLE VII: Factorial results (n = 218). The simple effect of the state shift is +74 problems; the simple effect of loss weighting is −7-7 (average main effects +68+68 and −13-13), and weighting still lowers the pass rate on top of the shift (191 to 172). Configuration State shift End-step weight Certified passes (n = 218) Δ vs. baseline Baseline (Exp. 3) No 1.0 117 — Weighted No 5.0 110 −7-7 Weighted + shift Yes 5.0 172 +55 Shift (final configuration) Yes 1.0 191 +74 These results show that adding information does far more than reallocating loss: correcting the state timing alone lifts the pass rate from 53.7% to 87.6%, whereas up-weighting the loss at the site where errors concentrate is negative under both states and raises confidently wrong decisions from 55 to 69. Weighting adds no decision-relevant information; it only shifts the tendency of the class prior. The migration of error composition tracks the completeness of state information (Figs. 4(a) and 4(b)): the final configuration’s 27 errors all sit at the final step and all are confusions between the square class and the other class (zero-residual verdicts are all correct, 31/31; zero-class-related confusions fall from 36 to 0; confidently wrong decisions fall from 55 to 12). The zero-residual case can be read directly off the residual value, while the square verdict requires the model to look up one of six squares, a representation-learning problem under information already in hand rather than missing information. Per-step decision entropy quantifies this structure: early-chain decisions are near-deterministic (entropy below 0.001 nats) and real uncertainty concentrates in the last three steps; failing problems have seven times the entropy of passing problems at the first divergent step (0.191 versus 0.027 nats), while the top-1 probability at that step still reaches 0.918 (Fig. 4(c)), so measurable extra uncertainty and high-confidence error hold at once. Two further pieces of parameter-side evidence appear in the appendix: the parameter geometry of the operator head separates backbone operators from added operators rather than clustering by problem family (Fig. A3); the two-dimensional loss cross-section at the training convergence point is a wide, shallow basin, with corner loss 15.2 times the convergence-point loss (Fig. A4); complete versions of the first-error probability and the along-chain entropy appear in Figs. A5 and A6. Fig. 4: Composition, confidence, and uncertainty of final-step errors. (a) All 101 baseline first errors sit at the chain’s final step, and the 27 remaining errors of the final configuration are all table-lookup confusions between the square class and the other class, with all zero-residual verdicts correct (31/31). (b) Distributions of top-1 probability at the first erroneous decision step: the two configurations’ shapes nearly coincide, and confidently wrong decisions fall from 55 to 12; the state shift changes the number of errors, not their confidence. (c) Decision entropy along the chain: early steps are near-deterministic (below 0.001 nats), real uncertainty concentrates in the last three steps, and failing problems have seven times the entropy of passing problems at the first divergent step (0.191 versus 0.027 nats). IX Cross-Model Examination and Scale Decomposition Once the two laws closed on the same exam, two questions followed: is the collapse specific to small models, and what are the separate contributions of the architectural change and of model scale? Experiment 5 evaluates DeepSeek-Prover-V1.5-RL [3] (7B parameters, int8 quantization, greedy decoding, zero-shot prompting, single generation) on the same 218-problem suite. Certified passes: 18/218 (8.3%); 177 outputs contain an unsolved goal (sorry), and 23 are rejected by the review program. By family: nested induction 0/13, lemma tower 0/24, and every pass belongs to the sum-of-squares family (18/181). The final configuration of this paper reaches 191/218 on the same suite (Fig. 5(a)). The distribution of decision steps per problem appears in Fig. A7 (mean 6.12, chains of 5 to 9 steps; the two synthetic families have rigid chain lengths, and in the final configuration every remaining failure sits in the sum-of-squares family, Section VIII). This comparison must be read with the interface difference in view: the comparison model has no execution engine or compiler and must generate the complete proof as free text, so its failure mode matches the direct-generation experiments of Section VI; the suite demands more correctly written content integers than the model can produce. We therefore read this comparison as evidence on the structure of the output channel, not as a ranking of the two models’ reasoning ability. Table VIII gives the resource comparison. A cross-generation recheck of the comparison uses a bidirectional dual suite: DeepSeek-Prover-V2-7B [31] (int4 quantization, greedy decoding, single generation capped at 8,192 tokens) answers both the main suite of this paper (218 problems) and a stratified suite of 500 rows drawn from the public library Lean-Workbook [8], with problem sources and style close to that model family, so that a favorable skew of the exam cannot explain the comparison result. Both suites yield zero certified passes (0/218 and 0/500; Wilson 95% upper bounds 0.017 and 0.008), and failing outputs almost all terminate in unsolved goals; generation-capacity triggers account for 77/218 and 177/500, and the problems that did not hit the cap (141 and 323) also all fail, so the zeros cannot be attributed to the generation budget. If the zeros simply reflected a domain mismatch, the model should do clearly better on the stratified suite close to its own problem sources; the measurement says otherwise. The preset failure decomposition (correlation of content-integer count with correctness) degenerates because both arms are constant at zero, and yields no readable quantity. This configuration generates 5,255 tokens per problem on average (3,919 of them in the thinking segment), takes 286 s, and peaks at 11,649 MiB; both generation volume and wall-clock are an order of magnitude above V1.5-RL. The readings of the two generations on the same main suite (18/218 and 0/218) with consistent interruption patterns show that the iteration did not change the fate of the direct-generation paradigm on this class of propositions. All verdicts came from the version-frozen review program, with matching checksums before and after grading. Fig. 5: Main results. (a) Certified pass-rate ladder of the main configurations: 0/218 (direct generation), 1/218 (slotting), 117/218 (compilation), 191/218 (state shift), with the shallow-chain reference 180/1083 and the comparison model 18/218 marked. (b) Resource comparison (log axis): generated tokens per problem (6.12 versus 168.0), wall-clock per problem (0.53 s versus 19.88 s), and peak memory (833 MiB versus 8,567 MiB); the comparison model runs one to two orders of magnitude higher on all three. (c) The three-tier triage funnel over the full Lean-Workbook library (132,378→48,106→3,536132,378→ 48,106→ 3,536, with 2,132 certified). (d) End-to-end comparison of model-independent chain walking against type-tree chains over the nine extension families (45.10% versus 44.07%). TABLE VIII: Resource comparison (n = 218). V1.5-RL and V2 denote DeepSeek-Prover-V1.5-RL and DeepSeek-Prover-V2-7B; the ratio column is each generation against this architecture; the V2 column is under int4 quantization with single generation capped at 8,192 tokens. This architecture produces no natural-language thinking text; 6.12 is the mean number of decision actions per problem. Metric This architecture (135M) V1.5-RL (7B) V2-7B (int4) Ratio (V1.5 / V2) Certified passes 191/218 (87.6%) 18/218 (8.3%) 0/218 — Generated tokens per problem 6.12 (decision steps) 168.0 (output); 156.6 (input) 5254.6 (output, incl. 3918.8 thinking); 217.6 (input) 27.5×27.5× / 858×858× Wall-clock per problem 0.53 s 19.88 s 285.9 s 37.5×37.5× / 539×539× Peak inference memory 833 MiB 8567 MiB 11,649 MiB 10.3×10.3× / 14.0×14.0× Both ratios can be explained by the cost structures at the two ends. Per problem, the number of model forward passes and of engine calls each equals the number of decision steps T; the text is compiled from templates and never enters the generation sampling loop, so the per-problem cost of this architecture is Csc=T(cfwd+cexec)+ccompile,C_sc=T\,(c_fwd+c_exec)+c_compile, (21) where cfwdc_fwd is the cost of one forward pass, cexecc_exec the cost of one engine execution, and ccompilec_compile the cost of expanding the whole chain from templates; all three are deterministic and do not fluctuate with sampling. The direct-generation paradigm must generate every content integer digit by digit; its per-problem cost is Cdir=Ngenctok,C_dir=N_gen\,c_tok, (22) where ctokc_tok is the cost of one generated token, and the measured mean of NgenN_gen is 168.0 (V1.5-RL) and 5,254.6 (V2, including the thinking segment). The two cost expressions count different things: our corpus chains run 5 to 9 steps (mean 6.58), while the comparison models average 168.0 and 5,254.6 generated tokens; the measured ratios of Table VIII agree with this difference in counts (Fig. 5(b)). Injecting the same step-by-step state information as our system into the external comparison model gives pass rates of 18, 14, and 13 out of 218, no improvement. A three-configuration comparison gives a preliminary separation of the effect of scale alone: the inherited-head 135M, the new-head 1B, and the same-loadout new-head 135M reach 191, 170, and 180 out of 218; loadout migration and backbone scale each contribute about half the difference (−11-11 and −10-10 problems), and the two factors act on disjoint problem sets. Together with the attention ablation of the shallow-chain era (Section V), these two groups of results say: the collapse is not limited to small models, mechanism upgrades do not move the pass rate, and information visibility is the decisive variable. X Domain Extension: Validation on a Public Problem Library All experiments so far ran inside the proposition domain constructed by this paper and on the 218-problem main suite. To examine whether the recipe transfers and what the admissible domain actually covers, we extend the operator library and the corpus to the public library Lean-Workbook (139,826 problems) [8]. The extension follows the same discipline as the main suite: training data are synthesized by problem-family generalization, and every library problem is checked for leakage against problem name, statement text, and constant vector; the checking program itself is validated by injection experiments; the exams always use one deterministic renderer, and every problem is graded by the same frozen review program. On Lean-Workbook, 7,448 rows shipped with the library cannot be parsed, matching the exclusion count in the library’s documentation; they do not enter the denominator, and the remaining 132,378 rows form the full denominator. Structural triage produces three tiers: 48,106 rows admissible under our operator system; 84,267 rows parseable but without a matching problem family; and 5 rows failing to parse (Fig. 5(c)). Within the admissible domain, fixture-renderable chains exist for 3,536 rows, which enter review, and 2,132 certify (60.29%, Wilson 95% interval 58.67 to 61.89); the reference arm of the existing operator families stands at 73.04%, and the type-tree chains of the nine extension families at 44.07%. Rows outside the admissible domain are listed separately and do not enter the score. This coverage boundary is set by mechanical checks: which problems lie inside the capability domain, which do not, and why, are themselves outputs the system can produce. Part of the chains behind these whole-library readings comes from the fixture and the type trees. To isolate the model’s independent contribution, we run a model-independent chain-walking exam on 1,535 certifiable rows of the nine extension families, none of which intersects the training corpus. The model decides autonomously throughout, including the terminator; on the 623 rows whose chains are renderable, 281 certify (45.10%, Wilson 41.24 to 49.03), the same level as the type-tree chains at 44.07% (Fig. 5(d)). Of these, 331 rows match the fixture’s reference chains exactly, and the rendered text of these rows matches the fixture rendering line for line by checksum (331/331), ruling out systematic drift in the rendering channel. The deep-exam reading of 191/218 (87.6%) holds under the same-distribution condition: domain-extension training causes zero regression on existing capability, and the difference against the re-measured starting model is −5-5 problems; the discordant pairs b=4b=4 (the re-measurement passes while the new configuration fails) and c=9c=9 (the reverse) give the exact binomial test p=min[1, 2 1−(b+c)∑i=0min(b,c)(b+ci)]p= \! [1,\;2^\,1-(b+c) _i=0 (b,c) b+ci ] (23) Substituting gives p = 0.267; the difference is not statistically significant. The construction of the formula: under the null hypothesis (equal pass rates), the directions of the b+cb+c discordant pairs are independent and equiprobable, so the null distribution of the smaller-side count X=min(b,c)X= (b,c) is binomial B(b+c,1/2)B(b+c,1/2); the two-sided exact probability is 2P(X≤min(b,c))2\,P(X≤ (b,c)), capped at 1. With b=4b=4 and c=9c=9 there are 13 discordant pairs: ∑i=04(13i)=1+13+78+286+715=1,093 _i=0^4 13i=1+13+78+286+715=1,093, so p = 2×1093/2132× 1093/2^13 = 0.267, consistent with (23). One negative result is reported in full. Merging the corpus of the existing routing families into training, so that routing problems enter the model’s capability domain, fails the zero-regression gate in all three mixing ratios (176, 184, and 172 out of 218, all below 191), with degradation not monotone in the ratio; we register this as a sensitivity of corpus mixing to the training trajectory, and model-level inclusion of the routing domain is left to future methodological work. In the whole-library readings, this domain’s score comes from the fixture reference arm and is labeled as such. All readings additionally passed an independent final audit: stratified re-grading by independent judges with zero discrepancies, and item-by-item reconciliation of discordant rows and denominator scope. XI Discussion The two empirical laws merge into one design principle: for multi-step numeric derivation, restrict the model’s free-generation range and make the tool state needed for the verdict available at decision time. The first law says that when numeric content is generated freely, the required accuracy grows exponentially with the length of the proposition, and improving per-element accuracy cannot compensate; the second says that inside a restricted decision space, information visibility rather than loss allocation decides correctness. The experimental results agree with the division-of-labor hypothesis of the introduction, and the architecture choice both point to is: the model handles policy (choosing steps and arguments), the symbolic tool handles computation, and template compilation handles text. The analysis of the error structure also carries independent evaluation significance. Token-level accuracy and the surface correctness of chain-of-thought intermediate steps can badly overestimate ability on long-derivation tasks; in settings where proof validity is a Boolean conjunction, per-content-element accuracy and the element count are the quantities directly tied to the pass rate; the controlled-corruption experiment further shows that the load-bearing integer count is what matters: when non-load-bearing numbers are present (which depends on the proof template), the measured pass rate runs above the value computed from the surface count. This analysis also offers a way to read the failure samples of other direct-generation systems: the interruption patterns of the two comparison generations on this suite match our direct-generation experiments (177 sorry interruptions for V1.5-RL; near-total sorry interruptions for V2-7B on both suites) and are explained by the conjunctive requirement on content elements, without assuming insufficient model scale. For tool-augmented methods, our results emphasize the timing and content of tool-state feedback, beyond the availability of tools. In our factorial experiment the tool, the execution engine, is available in every configuration; the only difference is the computation timing of the state inside the decision frame, and that single difference moves the pass rate by 74 problems. This suggests that in settings with step-by-step tool calls, the design of state feedback should be evaluated as an independent design variable. The separate effect of scale has been separated in a first approximation by the three-configuration comparison: loadout migration and backbone scale each contribute about half the difference (−11-11 and −10-10 problems, Section IX), whereas within this domain the combined effect of removing free generation and completing state information (from near zero to 87.6%) far exceeds the parameter gap between the two backbones in the comparison; this contrast in magnitude is the substance of our claim. Replication on larger backbones and transfer of the recipe to more problem families remain future work. The auditability of this architecture is not a bolted-on engineering measure but a direct consequence of separating responsibilities: the model’s output is restricted to symbolic decisions, computation lives in a deterministic engine, and text comes from template compilation; each can be checked independently. This makes both the failures and the successes of the system explainable down to specific stages; our localization of the error structure (Section VI) and of state timing (Section VIII) both rest on this property. Extracting human-readable symbolic accounts from trained networks is an active direction [32]; here the symbolic account is native to the architecture. For applications that need reliability guarantees, this property has value independent of the pass rate; formal verification of neural networks is an established line in this journal [33], [34], and auditability extends the same concern from the network to the process that generates its outputs. The structured process also changes how evaluation and scrutiny work. When the smallest unit of model behavior is an executable operator decision, a failure sample no longer offers only an aggregate signal but decomposes into position (which step failed), content (which argument or class failed), and confidence (the decision distribution); the error localization and attribution of Section VIII are built on this decomposition. For applications that presuppose reliability, this property matters as much as the pass rate itself: it allows mechanical enumeration and statistics of failure modes before deployment, without human sampling of generated text. Unlike chain-of-thought, this observability costs no natural-language output: the final configuration completes the entire solution within 6.12 discrete decision actions per problem on average, and the model generates no text to explain itself. XII Limitations This paper has several main limitations. The problem domain consists of constructively generated discrete-mathematics problems in three families (induction, inequalities, number theory); the conclusions do not transfer directly to open domains or to propositions requiring complex lemma rewriting. The main test suite has 218 problems and comes from our own generators; although zero-capability controls, semantic overlap filtering, and stating graded counts with every reading are in place, and the domain-extension validation on the public library (Section X) adds external readings, most rows of Lean-Workbook (84,267 of 132,378) lie outside the admissible domain of our operator system, and further extension of that domain is constrained by corpus-mixing sensitivity (the negative result at the end of Section X). Experiments use SmolLM2-135M as the main backbone; the three-configuration comparison on the 1B backbone (Section IX) gives a preliminary split of loadout migration and scale at roughly half each, and systematic validation at larger scale is still pending. Review verdicts are bound to our frozen review program and Lean version; changing the proof assistant or the version requires redoing the dual-protocol recheck. Finally, the external models in the comparison experiments are not connected to our toolchain; the comparison speaks to the difference in output-channel structure and cannot be read as a same-interface comparison of the two models’ ability. XIII Conclusion This paper examined the failure mechanism of long-chain generation in language-model automated theorem proving inside a fully auditable discrete-mathematics domain, and proposed SCOPE, an architecture with the model as policy planner. The main results follow. Under direct generation of complete proofs, the pass rate is bounded by a power law in the accuracy of single content elements, and token-level accuracy diverges from the pass rate (token accuracy 0.9637 with 0/218 passing; the control-set pass rate matches the power-law prediction, and the controlled-corruption experiment verifies the constraint on 2,617 reference proofs, with load-bearing corruption surviving 0/432). Replacing free-text generation with a compiler raises the pass rate from 1/218 to 117/218, and the text stage stops costing anything. A factorial experiment on final-step decisions shows that the state timing of the decision frame alone determines a 74-problem difference in pass rate (117/218 versus 191/218), while loss weighting is negative. On the same suite, the 135M configuration with the toolchain attached reaches an 87.6% certified pass rate at one to three orders of magnitude lower resource cost than two generations of 7B proof-specialized direct generators, and the cross-generation recheck points the same way (V2-7B certifies zero on both the main suite and the public-library stratified suite, including the problems that never hit the generation cap). All multi-step thinking happens in the discrete decision sequence, with no natural-language thinking text. We conclude that in multi-step numeric derivation, output-channel structure and decision-information visibility are more direct improvement variables than model scale. On the public library, domain extension reaches a 60.29% certified pass rate on gradeable problems inside the admissible domain with zero regression on the old domain, and model-independent pass rates on the extension families match the fixture chains; systematic validation on larger backbones is future work. Appendix A Figure and Table Inventory with Data Sources The five main figures are numbered in order of appearance. Fig. 1, the SCOPE architecture and data flow (division of labor among the three components, the zero-token thinking label, and the main readings); Fig. 2, the low-dimensional projection of decision-frame hidden states (the measured family organization and chain progression); Fig. 3, quantitative tests of Law 1 (the power-law curve with measured points, and the two controlled-corruption panels); Fig. 4, composition, confidence, and per-step entropy of final-step errors (three panels); Fig. 5, the main results grid (configuration pass-rate ladder, resource comparison, the Lean-Workbook triage funnel, and the nine-family end-to-end comparison). The carrier-comparison readings of multi-hop latent readout are carried by Table IV and the text of Section IV-A and are not given a separate figure. Seven appendix figures follow: Fig. A1, training dynamics of the final configuration (loss components and gradient norms, 6,000 steps); Fig. A2, the depth-curriculum ladder of the discretization experiment (gate-probe trajectory, Section IV-A); Fig. A3, the vocabulary geometry of the operator-selection head (separation of backbone and added operators, not family clustering); Fig. A4, the filtered-direction loss cross-section at the training convergence point (51×5151× 51 grid, a wide shallow basin); Fig. A5, complete two-configuration distributions of first-error probability (the full version of Fig. 4(b)); Fig. A6, the complete along-chain decision-entropy curves (the full version of Fig. 4(c)); Fig. A7, decision-step counts and per-family pass rates (Section IX). Per-figure data files for every figure (with source paths and checksums) live in writing/figures/llm_analysis/ of the code repository; drawing notes are in writing/FIGURES_PLAN.md; every number can be exported directly from the raw files of the results and gen44 directories. The eight tables are numbered in order of appearance: Table I, problem-domain layers and the operator vocabulary; Table I, execution logic of representative operators; Table I, step-by-step computation of a sum-of-squares problem; Table IV, carrier comparison for multi-hop latent readout; Table V, mechanism decomposition of the discretization experiment; Table VI, main experimental configurations; Table VII, factorial results; Table VIII, resource comparison. Data sources as above. Appendix B Review Program and Key-File Checksums The review program source is drct_common.py, version-frozen for the entire experimental period, MD5 7c31b58da9d7228cee31b9be581fe5d. The raw reading files of every experiment (per-problem records, stratified rechecks, and reverse-verification results) and their checksums are listed in MANIFEST.md and the results directory of the code repository; training configurations and batch-order checksums are recorded in the report file of each experiment. The key files of the domain-extension and public-library validation (the final experiment report, the literal-scope full re-grading summary, the final-exam model checkpoint, and the final-audit report) and their checksums are in the gen44 directory; the key files of the cross-model dual-suite comparison (the experiment report, the grading summary, and the failure-decomposition artifacts) and their checksums are in the gen45 directory. Fig. A1: Training dynamics of the final configuration (6,000 steps). (a) Total objective with the chain and slot components (log axis). (b) Clipped gradient norm and held-out operator top-1 accuracy; the latter saturates from step 50 onward, so training progress is read from the loss. Fig. A2: The depth-curriculum ladder of the discretization experiment (v15). (a) The gate-probe measured depth rises monotonically from 1 to 16, with all fifteen openings between training steps 11,000 and 17,500; the shading shows depth sampling of training episodes. (b) Probe and training error curves. (c) Depth sampling of training episodes. Fig. A3: Low-dimensional projection of the operator-selection head’s output vectors (220 rows). The head encodes the boundary between backbone and added operators (0.969 within-backbone nearest-neighbor share), not a seven-segment clustering by problem family. Fig. A4: Filtered-direction loss cross-section at the training convergence point (51×5151× 51 grid). The floor is 0.235 nats; the corners reach 5.34 nats, 15.2 times the loss at the convergence point (0.351 nats), forming a wide, shallow basin. Fig. A5: Empirical distributions and counts of top-1 probability at the first erroneous decision step in the two configurations (baseline n = 101, final configuration n = 27; counts at the 0.9 threshold: 55 and 12); the full version of Fig. 4(b). Fig. A6: Operator-decision entropy along the chain (log vertical axis; certified passes versus failures), the full version of Fig. 4(c); at t=4t=4 the two groups read 0.0270.027 and 0.1910.191 nats. Fig. A7: Step-count distribution of the 218 gold operator chains (stacked by problem family, mean 6.12), and the compile-grade pass rate of each family for the Experiment 2 chains under compilation (121/218: nested induction 13/13, lemma tower 24/24, sum-of-squares 84/181). References [1] L. de Moura and S. Ullrich, “The Lean 4 theorem prover and programming language,” in Proc. 28th Int. Conf. Automated Deduction (CADE), Lecture Notes in Computer Science, vol. 12699, 2021, p. 625–635. [2] L. B. Allal et al., “SmolLM2: When smol goes big: Data-centric training of a small language model,” arXiv preprint arXiv:2502.02737, 2025. [3] H. Xin et al., “DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and Monte-Carlo tree search,” arXiv preprint arXiv:2408.08152, 2024. [4] S. Polu and I. Sutskever, “Generative language modeling for automated theorem proving,” arXiv preprint arXiv:2009.03393, 2020. [5] K. Yang et al., “LeanDojo: Theorem proving with retrieval-augmented language models,” in Advances in Neural Information Processing Systems (NeurIPS), 2023. [6] H. Xin et al., “DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data,” arXiv preprint arXiv:2405.14333, 2024. [7] K. Zheng, J. M. Han, and S. Polu, “MiniF2F: A cross-system benchmark for formal olympiad-level mathematics,” in Proc. Int. Conf. Learning Representations (ICLR), 2022. [8] H. Ying, Z. Wu, Y. Geng, J. Wang, D. Lin, and K. Chen, “Lean workbook: A large-scale Lean problem set formalized from natural language math problems,” arXiv preprint arXiv:2406.03847, 2024. [9] G. Lample et al., “HyperTree proof search for neural theorem proving,” in Advances in Neural Information Processing Systems (NeurIPS), 2022. [10] M. Mikuła et al., “Magnushammer: A transformer-based approach to premise selection,” in Proc. Int. Conf. Learning Representations (ICLR), 2024. [11] A. Q. Jiang et al., “Draft, sketch, and prove: Guiding formal theorem provers with informal proofs,” in Proc. Int. Conf. Learning Representations (ICLR), 2023. [12] T. H. Trinh, Y. Wu, Q. V. Le, H. He, and T. Luong, “Solving olympiad geometry without human demonstrations,” Nature, vol. 625, no. 7995, p. 476–482, 2024. [13] T. Hubert et al., “Olympiad-level formal mathematical reasoning with reinforcement learning,” Nature, vol. 651, no. 8106, p. 607–613, 2025. [14] E. First, M. N. Rabe, T. Ringer, and Y. Brun, “Baldur: Whole-proof generation and repair with large language models,” in Proc. 31st ACM Joint European Software Engineering Conf. and Symp. on the Foundations of Software Engineering (ESEC/FSE), 2023, p. 1229–1241. [15] P. Song, K. Yang, and A. Anandkumar, “Lean Copilot: Large language models as copilots for theorem proving in Lean,” in Proc. Int. Conf. Neuro-Symbolic Systems (NeuS), PMLR vol. 288, 2025, p. 144–169. [16] K. Su, H. Su, C. Li, J. Zhu, and B. Zhang, “Probabilistic neural–symbolic models with inductive posterior constraints,” IEEE Trans. Neural Netw. Learn. Syst., vol. 35, no. 2, p. 2667–2679, 2024. [17] L. Gao et al., “PAL: Program-aided language models,” in Proc. Int. Conf. Machine Learning (ICML), 2023. [18] T. Schick et al., “Toolformer: Language models can teach themselves to use tools,” in Advances in Neural Information Processing Systems (NeurIPS), 2023. [19] Y. Zhang, Z. He, and G. G. Yen, “Uncovering large language model weaknesses in character and word understanding and manipulating,” IEEE Trans. Neural Netw. Learn. Syst., vol. 36, no. 10, p. 17570–17584, 2025. [20] Y. Bengio, J. Louradour, R. Collobert, and J. Weston, “Curriculum learning,” in Proc. Int. Conf. Machine Learning (ICML), 2009, p. 41–48. [21] S. Bengio, O. Vinyals, N. Jaitly, and N. Shazeer, “Scheduled sampling for sequence prediction with recurrent neural networks,” in Advances in Neural Information Processing Systems (NeurIPS), 2015. [22] M. Ranzato, S. Chopra, M. Auli, and W. Zaremba, “Sequence level training with recurrent neural networks,” in Proc. Int. Conf. Learning Representations (ICLR), 2016. [23] N. Dziri et al., “Faith and fate: Limits of transformers on compositionality,” in Advances in Neural Information Processing Systems (NeurIPS), 2023. [24] H. Lightman et al., “Let’s verify step by step,” in Proc. Int. Conf. Learning Representations (ICLR), 2024. [25] J. Wei et al., “Chain-of-thought prompting elicits reasoning in large language models,” in Advances in Neural Information Processing Systems (NeurIPS), 2022. [26] A. Vaswani et al., “Attention is all you need,” in Advances in Neural Information Processing Systems (NeurIPS), 2017. [27] L. McInnes, J. Healy, and J. Melville, “UMAP: Uniform manifold approximation and projection for dimension reduction,” arXiv preprint arXiv:1802.03426, 2018. [28] S. Hao et al., “Training large language models to reason in a continuous latent space,” in Proc. Conf. on Language Modeling (COLM), 2025. [29] J. Geiping et al., “Scaling up test-time compute with latent reasoning: A recurrent depth approach,” in Advances in Neural Information Processing Systems (NeurIPS), 2025. [30] E. B. Wilson, “Probable inference, the law of succession, and statistical inference,” J. Amer. Statist. Assoc., vol. 22, no. 158, p. 209–212, 1927. [31] DeepSeek-AI, “DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition,” arXiv preprint arXiv:2504.21801, 2025. [32] J. Townsend, T. Chaton, and J. M. Monteiro, “Extracting relational explanations from deep neural networks: A survey from a neural-symbolic perspective,” IEEE Trans. Neural Netw. Learn. Syst., vol. 31, no. 9, p. 3456–3470, 2020. [33] W. Xiang, H.-D. Tran, and T. T. Johnson, “Output reachable set estimation and verification for multilayer neural networks,” IEEE Trans. Neural Netw. Learn. Syst., vol. 29, no. 11, p. 5777–5783, 2018. [34] F. Boudardara, A. Boussif, P.-J. Meyer, and M. Ghazel, “INNAbstract: An INN-based abstraction method for large-scale neural network verification,” IEEE Trans. Neural Netw. Learn. Syst., vol. 35, no. 12, p. 18455–18469, 2024.