LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization

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

scope and central result

LeanFlow treats document-to-formal-project work as a controlled workflow. It resolves a source, records a blueprint linking source spans to Lean declarations, audits statement fidelity before proof search, and then proves one queued declaration at a time under final build and hygiene checks. The paper’s core distinction is between a declaration that type-checks and a declaration that faithfully states the source theorem. “Compilation only shows that a declaration is well typed; it does not show that the declaration is the theorem stated in the paper.” (Section 3, p. 3.)

The system has two document-level case studies: a Pythagorean-polynomial paper and a Cramer–Wold paper. The completed projects contain 83 declarations (34 theorem/lemma statements) and 114 declarations (101 theorem/lemma statements), respectively; both build sorry-free and without unapproved axioms (Section 5.1, p. 6). In Kimi-K2.6 runs with a 2,000-call prover budget, the full queue workflow succeeds in 1,043 calls and 1,278 calls, while all no-queue variants exhaust 2,000 calls and fail on both sources (Table 3, p. 7). GPT-5.5 completes all variants, so the paper treats queue effects for that model as efficiency/auditability evidence, not necessity evidence (Section 5.1, p. 7).

technique 1: deterministic source preflight and a durable blueprint

What it is. Before an agent writes Lean, LeanFlow resolves the source and pinned environment, extracts a manifest, and constructs a source-to-declaration map. The workflow contract says: “Resolve source document D and pinned Lean environment E.” and then “Extract a preflight manifest: source blocks, labels, references, PDFs, figures, and support files.” (Algorithm 1, p. 3.) For TEX directories it follows includes and rejects ambiguous roots; for PDFs it records extracted text, metadata, and image inventories using local Poppler tools (Section 4.2, p. 4).

When to use it. Use preflight when the input is a paper, repository, or multi-file specification whose identity, includes, figures, or environment can drift. A deterministic manifest makes later claims auditable and prevents an agent from silently reading a different root or dependency snapshot.

How to apply it. (1) Pin the checker/toolchain and project configuration. (2) Resolve the source root deterministically; reject ambiguity. (3) Extract theorem-like blocks, labels, references, nearby proof text, figures, and support files. (4) Create a blueprint mapping each source span to planned declarations, dependencies, source locators, proof notes, and scope changes. (5) Spell out drift-prone fields: type, quantifier order, domains, hypotheses, side conditions, codomain, and conclusion (Section 4.2, p. 4). (6) Generate a statement skeleton with sorry only in theorem-like proof bodies and require that the statement layer type-check before proof filling (Algorithm 1, p. 3).

Verus form. Inference: for VL, pin the Verus version, Rust toolchain, crate revision, and trusted library specifications; record source file, function, contract, and requirement spans in a machine-readable manifest. Inference: a blueprint can map requirement sentences to Rust functions, requires, ensures, spec fn definitions, and proof lemmas. Verus does not provide LeanFlow’s PDF/TEX extraction, so a separate parser or manually reviewed source map is needed.

Evidence and limits. LeanFlow’s completed projects are the evidence that this pre-proof bookkeeping can feed buildable artifacts (Section 5.1, p. 6). The authors state that the mathematical result should not depend on a particular environment snapshot, but build and diagnostics are always relative to the pinned environment E (Section 3, p. 3). Inference: changing Verus or dependency versions can change proof search and diagnostics even when the mathematical requirement is unchanged, so the environment belongs in the evidence record.

technique 2: statement/source fidelity gate

What it is. A separate reviewer checks whether generated declaration types preserve the source before proof search. The gate checks statement type, quantifiers, variable types, hypotheses, conclusion, encoding bridges, proof notes, and hygiene (Table 1, p. 4). “The statement/source gate checks the generated skeleton before proof search begins.” (Section 4.3, p. 4.) If any check fails, the formalizer redrafts the skeleton rather than letting the prover prove a weakened, strengthened, or incomparable claim.

When to use it. Use this gate whenever a generated formal statement could differ from the source while still compiling. It is essential for agent-generated specifications because proof completion cannot detect that the wrong theorem was encoded.

How to apply it. (1) Freeze the source blueprint, generated declarations, and source spans. (2) Launch a fresh reviewer context with no proof-filling role. (3) Compare type, quantifier order/dependencies, variable domains, hypotheses and nonemptiness conditions, conclusion (equality/equivalence/existence), encoding bridges, and proof notes against the source. (4) Reject and redraft on any mismatch. (5) Keep the reviewed skeleton fixed during proving; only proof bodies and local helper lemmas may change (Sections 4.3–4.4, p. 4). (6) Perform expert confirmation when the automated reviewer cannot guarantee faithfulness (Section 6, p. 10).

Verus form. Inference: apply the gate to every public Verus contract before proving: review requires, ensures, quantified variables, data domains, and assumptions against the requirement. Then freeze function signatures and contracts while proof bodies evolve. Inference: Verus’s verifier can prove a wrong contract just as Lean can; a separate reviewer or test oracle must check requirement fidelity. Do not treat compilation as specification validation.

Evidence and limits. The qualitative Pythagorean comparison shows that both no-review and reviewed skeletons build but formalize different Lean decisions (Section 5.6, p. 10). The paper cautions: “The statement/source gate runs autonomously, but we still confirm faithfulness by expert inspection, because there is currently no automated way to guarantee that a well-typed declaration matches the source.” (Section 6, p. 10.) Thus the gate improves auditability but does not remove human semantic judgment.

technique 3: two-layer declaration queues and failed-attempt memory

What it is. A project-wide queue chooses the next file using dependencies and hints; a file-scoped queue exposes one active declaration at a time. The manager stores target context, failed attempts, diagnostics, retry counters, verification records, and checkpoints. The paper says: “The file-scoped declaration queue keeps proof search focused by exposing only one active assignment at a time.” (Section 4.5, p. 5.)

When to use it. Use queue control for long projects with dependent declarations, many files, or limited model calls. It prevents the agent from proving later theorems before prerequisites, repeating failed proof shapes, or losing its target after context compaction.

How to apply it. (1) Scan project files and rank them by declaration dependencies, hints, examples, and size. (2) Assign one file, then build a queue from pending sorry declarations and diagnostics. (3) Expose only the front declaration. (4) Let the model search, edit, and verify that declaration. (5) Record each failed attempt, diagnostic, route decision, and checkpoint. (6) Accept an edit only after the declaration verifies; then advance. (7) Run final file/project build and hygiene scans for sorry, admit, unsafe, and unapproved axioms (Algorithm 1, p. 3; Sections 4.4–4.5, pp. 4–5).

Verus form. Inference: represent each proof obligation as a queue item keyed by function/lemma and dependency. Persist verifier diagnostics and failed attempts outside the model context. Verify only the active function or proof block, then run a crate-level check after successful advancement. Verus has no LeanProbe or declaration queue; a VL manager can orchestrate verus commands and retain the same state discipline.

Evidence. The Kimi-K2.6 ablation uses four workflows and a 2,000-call cap per source. Full LeanFlow succeeds at 1,043 calls (Pythagorean) and 1,278 (Cramer–Wold); NoQ+Tools, Q+CLI, and NoQ+CLI each fail at 2,000 calls for at least one source, with all no-queue variants failing both (Table 3, p. 7). The queue/tool effects are model-dependent: GPT-5.5 succeeds in all 16 document-level cells (four workflows × two sources) (Table 3, p. 7). Inference: queueing reduces wasted search for some models but is not itself a proof guarantee.

technique 4: verifier-backed local repair with LeanProbe

What it is. LeanProbe checks candidate proof replacements in a cached environment and returns local goals and diagnostics before the next model attempt. Accepted declarations advance the environment; failed candidates do not alter later context. The tool surface includes source readers, file editing, Lean verification, structured search/context, proof exploration, hygiene scans, workflow memory, and terminal fallback (Table 2, p. 5).

How to apply it. (1) Prepare the current environment once. (2) Replace only the active declaration’s proof. (3) Run a cached target check. (4) Return residual goals and diagnostics beside the failing tactic. (5) Record the failure; either revise the same target or restore a baseline sorry. (6) Advance the environment only after a complete declaration succeeds (Sections 4.5–4.6, pp. 5–6).

Verus form. Inference: use verus on a narrowed module or function where possible, capture diagnostics, and preserve a known-good baseline. Inference: local checks should not mutate later proof context after a failed candidate; this mirrors Verus’s need to avoid accidentally relying on an unverified edit. Verus proof functions remain erased from runtime, and executable functions must carry the actual contracts being checked.

Evidence. On the RLM25-PFR slice, GPT-5.5 LeanFlow has 81.2% proof success, 70.8% BEq, and 75.7% BEq+ with 3,541 total calls; terminal-only has 80.6%, 68.1%, and 72.9% with 4,053 calls (Table 4, p. 7). The paper reports one measured run, so it treats the BEq+ difference as a small effect rather than a significance claim (Section 5.3, p. 7). LeanProbe latency benchmarks show cached repeated-target checks in hundredths of a second versus fresh checks in seconds (Table 6, p. 8), but these are tool measurements, not end-to-end proof guarantees.

what is proved, measured, and trusted

A final Lean/Lake build proves that the generated project type-checks and has completed proofs under the pinned environment; hygiene checks establish absence of forbidden placeholders and axioms. BEq/BEq+ measure statement similarity to reference formal statements. Call and token totals measure model-side effort. The paper explicitly separates success from semantic fidelity: “a proved declaration can still formalize the wrong mathematical claim.” (Section 5.3, p. 7.)

Inference: trusted components include the source extraction and blueprint, reviewer judgment, Lean kernel and libraries, environment pinning, the source theorem itself, and any external definitions or axioms permitted by policy. Inference: for VL, the greatest product threat is contract/API drift hidden behind a valid Verus proof; the most direct mitigation is a pre-proof source gate and immutable proof targets. The paper’s queue, local feedback, and hygiene workflow is directly reusable, while its Lean-specific tools and mathematical benchmarks are not evidence about Rust systems performance.

Inference: VL should not redo the generic result that verifier feedback helps agents repair proofs. A useful new measurement would be the rate and cost of contract repairs caught by a source gate before Verus proving, with denominators split by requirement type and model. The paper’s own threats remain: document-level ablations are single runs, mechanisms are bundled, only two source case studies are used, and no matched document-level baseline is included (Section 6, p. 10).

techniques for the catalog

• deterministic source preflight and blueprint — pin the environment, extract source artifacts, and map source spans to planned declarations
• statement/source fidelity gate — audit generated types and assumptions before proof search, then freeze accepted targets
• two-layer declaration queue — route dependent files and expose one active declaration while persisting failures and checkpoints
• verifier-backed local repair — test one candidate proof in a cached environment and advance only after a clean check

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numbers, references, techniques, and conclusions against the full paper; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15