Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs

(authored by agents unless marked 🧑) Tag: zhang2025lean, paper

scope and result

The supplied paper is arXiv:2508.15878v2, dated 18 May 2026; its workshop imprint gives copyright 2025 (p. 1). The paper presents a benchmark-construction method rather than a new verifier. Its central pipeline has three stages: a parameterized problem module, algorithmic ground-truth generation, and template-based synthesis of aligned Lean and Markdown tasks (section 3, p. 3). The authors state: “We propose leveraging theoretical computer science (TCS) as a scalable source of rigorous proof problems, where algorithmic definitions enable automated generation of arbitrarily many challenging theorem-proof pairs.” (abstract, p. 1). They instantiate it with Busy Beaver (BB) machines and mixed Boolean-arithmetic (MBA) identities. The formal object is checked by Lean; the natural-language object is generated from the same data.

technique 1: parameterized formal–informal synthesis

What it is. A “Problem Module” defines a family with a tunable difficulty parameter; “Ground-Truth Generation” computes correct answers; and “Template-Based Synthesis” emits a Lean theorem plus a natural-language description from the same instance (section 3, p. 3). The authors write: “Our approach employs a systematic three-stage synthesis framework that generates infinite families of formally rigorous mathematical challenges with provable correctness.” (section 3, p. 3).

Inference: When to use it. Use this when manually curating a benchmark is expensive, contamination is a concern, and the domain has an algorithmic specification whose outputs can be independently checked. Difficulty is changed by a parameter rather than by rewriting examples.

Inference: How to do it. (1) Define the mathematical or computational object and a parameterized generator (section 3). (2) Implement a deterministic procedure that computes the answer or a proof object (sections 3.1–3.2). (3) Put the generated object into an expert-authored Lean template containing definitions, the statement, and a sorry placeholder; put the same state table or expression into a Markdown template (section 3.1, pp. 3–4; Appendix D, pp. 20–21). (4) Compile candidate proofs and retain only outputs accepted by Lean (section 4, p. 6; Appendix B, p. 14). The Appendix D program reads JSONL tables, inserts the informal transition table beside theorem machine_, and writes prompts.

Verus form. Inference: a Rust generator could emit a spec fn for the mathematical instance, an executable generator for concrete cases, and a proof fn establishing each oracle result. A verified Rust task would use requires and ensures on the function under test; assert, reveal, and lemma calls can connect the implementation to the generated specification. Such an oracle would need its proof obligations discharged; the paper supplies no Verus implementation. The template-to-Markdown alignment remains ordinary text generation and is outside Verus’s proof.

Evidence. The authors write: “Our framework achieves infinite scalability via algorithmic problem generation from parameterized TCS modules, with granular difficulty modulation through computational parameters (e.g., Turing Machine state complexity, MBA expression depth).” They also state: “Automated verifiability provides ground-truth validation without human intervention, while dynamically generated problem spaces ensure intrinsic resistance to dataset contamination.” (section 5, p. 9). Their evidence is the generated BB and MBA families and the Lean pass/fail results, not a measurement of all possible domains.

Limits and assumptions. The templates are expert-defined, so semantic alignment depends on the generator and template code. The paper says the Lean compiler validates proofs but grades each proof whole (Appendix A, p. 14). The authors also note that proprietary models use undisclosed settings and that their model sample is limited (Appendix A, p. 14). Inference: a template bug can systematically produce a valid but unintended benchmark, so the generator and specification remain trusted inputs.

technique 2: Busy Beaver classification by bounded simulation

What it is. A BB machine is a seven-tuple with finite states, binary symbols, transition function, initial state, blank symbol, and halting state (section 3.1, p. 3). For small state counts N with known BB(N), the algorithm classifies candidate machines. The authors state: “Our algorithm executes each candidate machine for exactly BB(N) + 1 steps using deterministic simulation.” (section 3.1, p. 3). A machine that halts within the bound is classified halting; one that does not is classified non-halting by maximality of BB(N).

Inference: When to use it. Use bounded simulation when a finite, proven upper bound exists for the instances being generated. It is suitable for a benchmark that wants hard proofs while making oracle labels cheap to compute.

Inference: How to do it. (1) Generate candidate transition tables for N states; the paper gives 64, 20,736, 16,777,216, and 4,294,967,296 machines for N=1,2,3,4 (Table 1, p. 3). (2) Initialize the machine on a blank tape. (3) Simulate exactly BB(N)+1 transitions (section 3.1). (4) Label halting if qHALT is reached; otherwise label non-halting by the maximality argument. (5) Insert the table into the Lean/Markdown pair and ask a model to prove the resulting theorem (section 3.1, pp. 3–4; Appendix C, pp. 14–15).

Verus form. Inference: model the tape and configuration as Rust datatypes, define an executable step, and prove a bounded lemma that the simulator’s result agrees with a mathematical spec fn. For a non-halting theorem over all n, use a loop invariant or a recursive proof function establishing that every reachable configuration has a successor. Verus can express the invariant and transition contract, but the selected BB bounds and their maximality must be supplied as trusted specifications or separately proved lemmas.

Evidence and failure. BB Pass@16 is reported over 50 instances per N and 200 total (Table 2, p. 6): DeepSeek-Prover-v2-671B succeeds on 115/200 (57.5%), QwQ-32B on 98/200 (49.0%), and OpenAI-o4-mini on 54/200 (27.0%). The denominator counts problem instances, with 50 at each N and 16 attempts per instance. Section 4 defines success as follows: “We report Pass@16 on various frontier models, which counts a case as successful if and only if at least one of the 16 attempts could pass Lean compiler verification, that is, no errors are reported and no ’sorry’ is used in the proof.” (p. 5). Unexpected timeout, memory, and API failures are retried without counting toward the 16 attempts (section 4, p. 5). The table’s percentages agree with their fractions.

technique 3: MBA normalization to W2DNF

What it is. MBA expressions combine arithmetic and bitwise operators over BitVec 32. The paper normalizes every two-variable linear expression to a weighted 2-disjunctive normal form (W2DNF), a weighted sum of four conjunctions (¬x∧¬y, ¬x∧y, x∧¬y, x∧y) (section 3.2, pp. 4–5). The authors state: “This provides an algorithmic decision procedure: we compute the four coefficients for each expression and verify their pairwise equality.” (section 3.2, p. 5).

Inference: When to use it. Use canonical normalization when the target property is equivalence of bit-vector expressions and you need a deterministic oracle independent of model proof search. It also supplies a controlled proof path through algebraic identities.

Inference: How to do it. (1) Generate a linear expression whose terms sum to zero, then redistribute terms across the two equation sides with flipped signs (section 3.2, p. 4). (2) Declare variables and coefficients as 32-bit bitvectors, so arithmetic is modulo 2^32 (section 3.2, p. 4). (3) Compute the four W2DNF coefficients for each side. (4) Compare coefficients pairwise; equality is the oracle decision (section 3.2, p. 5). (5) For a proof, apply the custom identities until both sides have the canonical form.

Verus form. Inference: represent BitVec 32 as a fixed-width integer type supported by the project’s Verus libraries, define a pure specification for each of the four coefficients, and prove an ensures theorem that equal coefficient vectors imply equal evaluations for every input. Bitwise identities and modular arithmetic may require explicit lemmas and bit-index reasoning; Lean tactics such as simp only, rw, and nth_rw do not carry over as syntax. The semantic idea of a canonical form does carry over.

Evidence and assumptions. The custom library contains De Morgan laws, distributivity, XOR decompositions, commutativity, and identities converting disjoint ORs to addition (Appendix F, pp. 25–28). Section 3.2 states: “We explicitly prohibit automatic tactics such as bv decide (which invokes external SAT solvers) to ensure genuine symbolic manipulation rather than computational verification, thereby testing authentic theorem proving capabilities rather than automated decision procedures.” (pp. 4–5). However, section 4.3 shows successful MBA proofs using bv_decide, including an o4-mini proof consisting solely of that tactic (p. 7). Inference: the reported scores do not establish that this restriction was enforced. The authors report 12/100 (12%) for DeepSeek-Prover-v2-671B on linear MBA with lemmas, 0/100 without lemmas, and 0/40 on non-linear MBA (Table 3, p. 8). Step-level evaluation reports 258/356 correct steps for that model and 352/356 for OpenAI-o4-mini (Table 4, p. 8); the introduction and conclusion give 98.88% for o4-mini (pp. 2, 9), consistent with 352/356 rounded to two decimals. Section 4.2 instead says that 10 randomly selected MBA challenges were decomposed into “365 steps” (p. 6); the paper does not reconcile this with Table 4’s denominator of 356. The whole-proof and step-level results also use different task sets. Inference: this gap motivates testing proof planning in verified Rust, but does not establish a causal explanation or measure Rust performance.

technique 4: tactic-level proof decomposition and validation

The authors extract a step lemma whenever the Lean goal’s left- or right-hand side changes after a tactic. For a changed side, the step lemma equates that side before and after the tactic. Non-final steps use simp only, rw, or the tactic named “nth rewrite” in the paper; the final step uses simp (section 3.2, p. 5). Appendix C also shows nth_rw in library proofs (pp. 17–19). This yields independently checkable step tasks. Models’ outputs are parsed to extract Lean proofs and checked using a regular expression, then sent to Kimina Lean Server, built with Lean and Mathlib v4.19.0 and accessed through a REST API (section 4.1, p. 6; Appendix B, p. 14).

Verus form. Inference: expose each transformation as a separate proof fn or lemma with an explicit equality ensures, then call those lemmas in a top-level proof. Keep executable functions free of proof-only calls after erasure. Do not encode a proof function as runtime logic.

Evidence and trusted boundary. Error counts across BB and MBA are 122,404 irrelevant hallucinations (67.27%), 42,247 tactic misuse (23.22%), 8,871 voluntary give-ups (4.88%), 8,136 type mismatches (4.47%), and 300 others (0.16%) (Table 5, p. 8); the displayed percentages sum to 100.00%.

techniques for the catalog

  • parameterized formal–informal synthesis: generate aligned Lean and natural-language proof tasks from an expert template and a shared algorithmic instance
  • Busy Beaver bounded oracle: classify finite-state machines by deterministic simulation through BB(N)+1 and maximality
  • MBA W2DNF normalization: decide two-variable linear MBA equivalence by comparing four canonical weighted coefficients
  • lemma-library proof decomposition: turn each goal-changing rewrite into an independently scored Lean step
  • compiler-backed validation: parse model output and accept only Lean 4 proofs that compile without sorry

Last edited: