LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization

# LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization
Source: [https://arxiv.org/html/2607.20503](https://arxiv.org/html/2607.20503)
###### Abstract

We present and evaluate LeanFlow, an LLM agent system specialized for translating mathematical papers into buildable Lean projects\. Recent verifier\-in\-the\-loop systems show that large formal artifacts can be produced, but it remains unclear which runtime mechanisms affect completion, auditability, or efficiency in document\-to\-project formalization\. We study this question through case studies on two previously unformalized mathematical papers in number theory and measure theory, using model, proof\-workflow, and toolset ablations with Kimi\-K2\.6 and GPT\-5\.5; we report task outcome, API calls, input tokens, and output tokens\. With Kimi\-K2\.6, the full workflow completes both document\-level projects within the 2000\-call budget, while no\-queue variants reach the budget limit; with GPT\-5\.5, all document\-level variants complete, and the full workflow has the lowest or tied\-lowest input\-token cost on both sources\. As complementary calibration, LeanFlow reaches 75\.7% BEq\+ on the PFR slice of RLM25 and solves all five ICML 2026 AI for Math TCS challenge projects in our GPT\-5\.5 runs\.

autoformalization, theorem proving, Lean, LLM agents, document\-level formalization, proof repair

## 1Introduction

Autoformalization is moving from isolated theorem translation toward turning whole mathematical sources into Lean projects\. Early language\-model formalization work focused on translating individual natural\-language statements into proof\-assistant syntax\(Wuet al\.,[2022](https://arxiv.org/html/2607.20503#bib.bib13)\), and many theorem\-proving benchmarks still ask the model to prove one supplied formal statement at a time\(Zhenget al\.,[2022](https://arxiv.org/html/2607.20503#bib.bib10); Azerbayevet al\.,[2023](https://arxiv.org/html/2607.20503#bib.bib14)\)\. A document\-level agent faces a different problem: it must convert mathematical prose,TeXstructure, references, definitions, and proofs into a buildable Lean project while preserving the intended statements and managing a long sequence of dependent proof obligations\. M2F\(Wanget al\.,[2026](https://arxiv.org/html/2607.20503#bib.bib1)\)and recent textbook\- or project\-scale systems\(Gloeckleet al\.,[2026](https://arxiv.org/html/2607.20503#bib.bib30); Math, Inc\.,[2025](https://arxiv.org/html/2607.20503#bib.bib20); Hariharanet al\.,[2026](https://arxiv.org/html/2607.20503#bib.bib32); Tsoukalaset al\.,[2026](https://arxiv.org/html/2607.20503#bib.bib31)\)show that verifier\-in\-the\-loop formalization can produce large Lean artifacts; we examine which parts of the runtime help agents keep the source claims fixed and finish the resulting proof work\.

Motivated by this document\-scale setting, we introduce LeanFlow as a Lean\-specific runtime that separates mathematical editing from workflow control\. It first runs a deterministic source preflight: the runtime resolves the input document, extracts or records source blocks, labels, references, PDFs, figures, and support files, and refuses ambiguousTeXroots before the model starts\. The formalizer then builds a blueprint, a project\-local source map linking source spans to planned Lean declarations, dependencies, proof notes, and recorded scope changes\. Before proof search, a statement/source gate checks that the generated declaration types still match the original source claims\. During proving, a programmatic workflow manager owns the theorem queue, failed\-attempt memory, retry budgets, verification records, logs, and checkpoints\. The model proposes edits and helper lemmas, while the manager assigns one target at a time and advances only after external Lean verification accepts the edit\.

This separation has different benefits across the two model settings in our experiments\. For Kimi\-K2\.6\(Moonshot AI,[2026](https://arxiv.org/html/2607.20503#bib.bib3)\), workflow control is decisive in our two document\-level runs: the full workflow finishes both sources, while no\-queue variants exhaust the call budget\. For GPT\-5\.5, all document\-level variants finish, so the observed benefit is not a binary success difference; the same structure instead improves token efficiency and preserves an explicit audit trail for the proof work\.

LeanFlow also introduces LeanProbe111[https://github\.com/epfl\-lara/LeanProbe](https://github.com/epfl-lara/LeanProbe), a cached same\-file verifier built on LeanInteract\(Poirouxet al\.,[2025b](https://arxiv.org/html/2607.20503#bib.bib2)\), for repeated proof\-repair checks\. LeanProbe gives the proving agent low\-latency diagnostics and proof\-state feedback while leaving final acceptance to standard Lean/Lake checks\. In the sequential same\-file benchmark summarized in[Table6](https://arxiv.org/html/2607.20503#S5.T6), cached checking is roughly 9–14×\\timesfaster than rerunning growing\-prefix Lake checks\.

Our main evaluation ablates LeanFlow on real document\-level formalizations, where the system must recover statements from source documents and then complete the resulting proof work\. We compare queue management with free\-running proof loops, full Lean tool access with terminal\-only interaction, and source\-blueprint checkpoints with direct source\-to\-code generation\. Proof\-only benchmarks remain useful calibration, but they provide the formal statement in advance and only test whether the system can replace the proof placeholder\. We therefore report RLM25\-PFR agent runs and the ICML 2026 AI for Math TCS challenge\(AI for Math Workshop,[2026](https://arxiv.org/html/2607.20503#bib.bib5)\)as complementary measurements\.

The two document\-level case studies are Frisch and Vaserstein’s*Parametrization of Pythagorean Triples by a Single Triple of Polynomials*\(Frisch and Vaserstein,[2007](https://arxiv.org/html/2607.20503#bib.bib6)\)and Lyons and Zumbrun’s*A Calculus Proof of the Cramer–Wold Theorem*\(Lyons and Zumbrun,[2017](https://arxiv.org/html/2607.20503#bib.bib7)\)\. The Pythagorean source combines integer\-valued polynomial definitions, an obstruction overℤ​\[x1,…,xn\]\\mathbb\{Z\}\[x\_\{1\},\\ldots,x\_\{n\}\], explicit rational\-polynomial witnesses, and custom plain\-TeXtheorem macros\. The Cramer–Wold source combines probability measures on Euclidean space, closed half\-space values, Crofton reconstruction of average\-distance functions, odd\-dimensional Laplacian inversion, and an even\-to\-odd embedding step\. These sources are short enough for controlled ablations, but they are still full mathematical papers with nontrivial definitions, representation choices, and proof dependencies\. Both require source\-aware definitions and reusable Lean infrastructure that the prose leaves implicit\.

This paper makes threemain contributions:

- •A document\-to\-project workflow for Lean formalization\. LeanFlow starts from a paper orTeXproject, records which source text supports each generated declaration, checks statements before proof search, and moves to the next theorem only after Lean accepts the current proof edit\.
- •A fast local verifier for proof repair\. LeanProbe caches the Lean environment before the current declaration and returns proof states and diagnostics through a CLI and MCP server; final acceptance remains a standard Lean/Lake build\.
- •An evaluation on full mathematical sources and proof\-only benchmarks\. We ablate queue control, tool access, and source checkpoints on two paper formalizations with Kimi\-K2\.6 and GPT\-5\.5, and report RLM25\-PFR and ICML 2026 AI for Math TCS challenge runs as calibration\.

We release on GitHub the[LeanFlow implementation](https://github.com/epfl-lara/LeanFlow),[LeanProbe verifier](https://github.com/epfl-lara/LeanProbe), and[generated case\-study projects](https://github.com/epfl-lara/AutoformalizedProjects)\.

## 2Related Work

#### Formal theorem proving with language models\.

Lean 4\(de Moura and Ullrich,[2021](https://arxiv.org/html/2607.20503#bib.bib8)\)and Mathlib\(The mathlib Community,[2020](https://arxiv.org/html/2607.20503#bib.bib9)\)provide the verification substrate for many recent neural theorem\-proving systems\. Benchmarks such as miniF2F\(Zhenget al\.,[2022](https://arxiv.org/html/2607.20503#bib.bib10)\), ProofNet\(Azerbayevet al\.,[2023](https://arxiv.org/html/2607.20503#bib.bib14)\), PutnamBench\(Tsoukalaset al\.,[2024](https://arxiv.org/html/2607.20503#bib.bib28)\), FormalMATH\(Yuet al\.,[2025](https://arxiv.org/html/2607.20503#bib.bib27)\), SorryDB\(Letsonet al\.,[2026](https://arxiv.org/html/2607.20503#bib.bib24)\), and VeriSoftBench\(Xinet al\.,[2026](https://arxiv.org/html/2607.20503#bib.bib25)\)measure different proof\-only or repository\-scale capabilities\. They provide useful calibration, but most start from an existing formal statement or repository context\. Our work instead studies the runtime needed when the source begins as mathematical prose, and the output must be a buildable project\.

#### Autoformalization across scales\.

Early LLM autoformalization work studied natural\-language\-to\-formal translation at theorem scale\(Wuet al\.,[2022](https://arxiv.org/html/2607.20503#bib.bib13)\); later work improved process supervision and evaluation for Lean statements\(Luet al\.,[2024](https://arxiv.org/html/2607.20503#bib.bib15); Poirouxet al\.,[2025c](https://arxiv.org/html/2607.20503#bib.bib16),[a](https://arxiv.org/html/2607.20503#bib.bib17)\)\. M2F\(Wanget al\.,[2026](https://arxiv.org/html/2607.20503#bib.bib1)\)and Automatic Textbook Formalization\(Gloeckleet al\.,[2026](https://arxiv.org/html/2607.20503#bib.bib30)\)formalize long mathematical sources into Lean projects, audit generated statements, and repair proofs under a pinned environment\. Math, Inc\.’s Gauss system is an autoformalization agent for large Lean projects\(Math, Inc\.,[2025](https://arxiv.org/html/2607.20503#bib.bib20)\)\. In the sphere\-packing project\(Hariharanet al\.,[2026](https://arxiv.org/html/2607.20503#bib.bib32)\), it helps complete a sorry\-free formalization of the dimension\-8 result from an existing blueprint and Lean development\. AlphaProof Nexus\(Tsoukalaset al\.,[2026](https://arxiv.org/html/2607.20503#bib.bib31)\)uses an agentic evolutionary framework for formal proof search over a large set of formalized conjectures\. Direct comparison with M2F is difficult from the currently available public artifacts: reproducing our document\-level runs under M2F would require the same source documents, model, Mathlib version, budget, prompts, workflow logs, tool surface, and final acceptance criteria\. Our study is smaller in document volume but different in emphasis: we isolate queue control, tool routing, statement handoff, and model\-side budget under the two model settings in our experiments\.

#### Lean tooling for agents\.

Retrieval and environment access are central to practical Lean proving\. LeanDojo\(Yanget al\.,[2023](https://arxiv.org/html/2607.20503#bib.bib11)\)studies retrieval\-augmented theorem proving, and LeanExplore\(Asher,[2025](https://arxiv.org/html/2607.20503#bib.bib12)\)provides search over Lean declarations\. LeanInteract\(Poirouxet al\.,[2025b](https://arxiv.org/html/2607.20503#bib.bib2)\)exposes a Python interface to Lean execution\. LeanFlow builds on this tool ecosystem but introduces LeanProbe as its own cached same\-file verifier for agent loops; final acceptance still comes from standard Lean/Lake verification\.

## 3Problem Setting

LetDDbe a mathematical source artifact: aLaTeXfile, a PDF, or a directory containing aTeXproject\. LetEEbe a pinned Lean environment: a Lean toolchain, a fixed mathematical\-library revision such as a Mathlib commit, and the Lake project configuration used for checking\. The mathematical result should not depend on this particular snapshot, but the evaluation of builds, diagnostics, imports, and available lemmas is always relative toEE\. The goal is to produce a Lean projectPPtogether with declaration\-level provenance\. For each generated declarationd∈Decl​\(P\)d\\in\\mathrm\{Decl\}\(P\), the workflow should record

π​\(d\)⊆Span​\(D\),\\pi\(d\)\\subseteq\\mathrm\{Span\}\(D\),whereπ​\(d\)\\pi\(d\)is the finite set of source spans, labels, sections, pages, equations, or bibliography references justifyingdd\.

We separate three checks\. Statement type\-checking asks whether the generated Lean declaration is well typed underEEwhen theorem\-like proof bodies are replaced by explicitsorryplaceholders\. Statement faithfulness asks whether that well\-typed declaration states the source claim, including statement type, quantifiers, domains, hypotheses, and conclusion\. Proof completion asks whether a faithful declaration has a complete proof with no unacceptable placeholders or custom axioms\. The final project gate is stricter than a theorem\-local check: the requested file or full Lake project must build underEE, and a hygiene scan must report no unapprovedsorry,admit,unsafe, or hidden axiom\.

Source artifact\.tex, PDF,TeXtreePreflightmanifestblocks, PDFs, refsBlueprintsource mapdeps, names, notesLean draftstatements withsorryproofsStatement/sourcegateapprove or redraftProver queueone declarationat a timeLeanProbecached checkswarm envFinal gatesLake buildsorry/axiomsWorkflow state recordFormal statementsredraftFormalizerProver

Figure 1:LeanFlow document\-to\-project pipeline\. Dashed regions separate the formalizer and prover phases; the green silo is the project\-local workflow state record shared by both\. The formalizer emits a well\-typed statement skeleton and a durable blueprint, and formal theorem statements pass through a statement/source gate before the prover queue attempts proof closure under verifier and hygiene gates\. The workflow state records activity, proof checkpoints, failed attempts, route decisions, prover plans, and outcomes, so redrafts and build failures persist outside the transient conversation state\.
## 4Method

### 4\.1Workflow Overview

[Figure1](https://arxiv.org/html/2607.20503#S3.F1)and[Algorithm1](https://arxiv.org/html/2607.20503#alg1)summarize the document\-to\-project contract\. LeanFlow uses two primary workflows:formalize, which turns a source document into source\-backed Lean declarations and proof plans, andprove, which repairs or completes Lean proofs until the requested file or project compiles successfully\. The workflows are deliberately separated\. Formalization may introduce definitions, names, imports, and theorem statements, but it stops at a proof skeleton with source\-backedsorrybodies\. Proof repair then treats those declarations as fixed targets: it may edit proof bodies and add local helper lemmas, but it may not modify theorem statements, add axioms, or leave the assigned proof partially solved\.

Algorithm 1LeanFlow agent workflow contract1:Resolve source document

DDand pinned Lean environment

EE\.

2:Extract a preflight manifest: source blocks, labels, references, PDFs, figures, and support files\.

3:Create a “blueprint” mapping source spans to planned declarations, dependencies, scope changes, and proof notes\.

4:Draft Lean declarations with placeholders only for theorem\-like proofs; verify that the statement layer type\-checks\.

5:Run a statement/source gate; if faithfulness fails, redraft before proof search\.

6:whilethe requested file or project still contains assigned proof obligationsdo

7:Assign one theorem\-like declaration from the queue\.

8:Use search, proof context, and LeanProbe\-backed checks to repair the assigned proof\.

9:Persist failures, diagnostics, route decisions, and proof checkpoints after each attempt\.

10:Accept the assignment only after verification, no relevantsorry, and an acceptable axiom profile\.

11:endwhile

### 4\.2Source\-Backed Skeleton Construction

LeanFlow begins by resolving the source deterministically using document processing tools\. For aTeXproject directory, deterministic preflight uses regular expression search to identify and select a main entry point, follow local includes, record bibliography files, figures, PDFs, and support files, and fail on ambiguous roots before the agent starts\. The same pass extracts standard theorem\-like environments, custom theorem declarations, plain\-TeXtheorem/proof blocks, labels, references, citations, section structure, and nearby proof environments when available\. For PDFs, it records extracted text, metadata, and image inventories through local Poppler tools such aspdftotext,pdfinfo, andpdfimages; the model reads this bounded source view throughread\_pdf\.

The*formalize*workflow next creates a project\-local blueprint before the proof skeleton is considered ready\. The blueprint is the durable source map for the run: it lists source statements, planned Lean names, dependencies, source locators, statement\-fidelity checks, proof notes, and known scope changes\. For each source theorem or lemma, it spells out the parts of the formal type that are most prone to drift: statement type, quantifier order, parameter domains, codomains, hypotheses, side conditions, and follow\-on equivalences\. The generated Lean module must type\-check with theorem bodies left asby sorry; proof filling is deferred until the statement/source gate has approved the skeleton\.

### 4\.3Statement/Source Gate

The statement/source gate checks the generated skeleton before proof search begins\. Compilation only shows that a declaration is well typed; it does not show that the declaration is the theorem stated in the paper\. LeanFlow therefore launches a fresh LLM reviewer context—a separate model context with no human in the loop—over the blueprint, generated Lean declarations, and original source spans\. The reviewer is a single invocation of a thinking model; it can approve, reject, or request redrafting, but it does not fill proof bodies\. If any check in[Table1](https://arxiv.org/html/2607.20503#S4.T1)fails, the formalizer returns to the skeleton before the*prove*workflow starts; the prover should not receive a weakened, strengthened, or incomparable target\. We call the version that passes this gate the*reviewed skeleton*\.

Table 1:Statement/source review checks applied before proof repair\.
### 4\.4Project\-wide Prover Queue

The project\-wide prover queue chooses which file the prover should work on next\. When a requested project still containssorry, the manager scans the files, ranks candidate files using declaration dependencies, local hints, examples, and size estimates, records the route decision, and hands one file to the file\-scoped declaration queue\. This outer queue is needed because document formalizations produce many dependent proof obligations\. Without route control, the agent can spend calls on the wrong file, revisit failed paths, or move to later work before earlier dependencies are stable\.

### 4\.5File\-Scoped Declaration Queue

[Figure2](https://arxiv.org/html/2607.20503#S4.F2)shows the declaration queue and repair loop inside an assigned file\. Once the project queue selects a file, the manager builds a file\-scoped declaration queue from pendingsorrydeclarations and diagnostics\. The front queue item becomes the active declaration; the prover loop repairs only that declaration before the manager advances to the next queue item\. For the active queue item, the manager stores the target, theorem\-local failed attempts and diagnostics, retry counters, and the latest verification record; it also tracks the remaining declarations in the file and each accepted or failed outcome\. It builds the bounded context shown to the model, runs or routes verification, and lets the model advance only after the assigned declaration is clean\. The model sees the current target, a small view of the remaining file work, relevant source/proof context, and theorem\-local failed attempts\.

The file\-scoped declaration queue keeps proof search focused by exposing only one active assignment at a time\. It prevents common long\-run failures: losing the active theorem after compaction, retrying a previously failed proof shape, changing a future statement, or advancing because a text search no longer findssorrywhile Lean still reports open goals\. After each edit, the proving LLM agent refreshes the structured Lean state and asks the manager whether to continue the same declaration, accept the edit, restore a baselinesorry, or assign the next declaration\.

Queue managertheorem assignmentContext toolsinspect, search, proof stateCandidate editproof or helperLeanProbe checkcached environmentclean?record failurereplanaccept editnext targetnoyes

Figure 2:File\-scoped proving loop\. Failed checks update theorem\-local memory; accepted edits advance to file/Lake verification sweeps\.LeanProbe feedback on a failed candidatetheoremadd\_comm\_candidate \(x y :Nat\) :
x \+ y = y \+ x :=by/\- <feedback\>
\-\- proof state:
x y :Nat
⊢\\vdashx \+ y = y \+ x</feedback\> \-/rfl/\- <feedback\>
\-\-error: tactic ’rfl’ failed
</feedback\> \-/Figure 3:Example LeanProbe feedback embedded into a failed Lean candidate\. The proof state is injected before the failing tactic \(green marker\) and the diagnostic after it \(red marker\); the failing tactic is underlined in red\.
### 4\.6LeanProbe and Tool Surface

LeanProbe is a declaration\-level verifier for repeated proof attempts in one Lean file\. It is a standalone CLI, Python library, and MCP server built on LeanInteract\(Poirouxet al\.,[2025b](https://arxiv.org/html/2607.20503#bib.bib2)\), and is openly available at[epfl\-lara/LeanProbe](https://github.com/epfl-lara/LeanProbe)\. At assignment time, LeanProbe runs a*prepare*step for the active declaration: it checks imports, the file header, and all prior declarations, then stores the resulting environment immediately before the target\. Each*check*step replaces the target declaration with one candidate proof or helper block and checks it against that cached environment\. The cache advances only after a complete declaration replacement is accepted, so failed candidates give diagnostics without changing the environment seen by later obligations\.

LeanProbe returns proof\-agent feedback: diagnostics, warnings,sorrydetection, tactic metadata, goal states, and inline Lean comments at the failing location\. A failed candidate can be returned as model\-readable Lean with compact comments containing the local proof state and the diagnostic beside the failing tactic, as illustrated in[Figure3](https://arxiv.org/html/2607.20503#S4.F3)\.

Table 2:Default tool surface exposed to the agent currently comprises 27 tools\. The following table groups them by purpose\. The manager decides which tool class is relevant for the current proof obligation or failure mode\.This information is used for fast local repair inside the queue loop, not for final acceptance\. The final gates remain module or project Lake builds and verification that the project is free from unapprovedaxiomdeclarations and remainingsorryplaceholders\.[Table2](https://arxiv.org/html/2607.20503#S4.T2)summarizes the tool classes exposed to the model; ablations in[Section5](https://arxiv.org/html/2607.20503#S5)remove this surface to isolate its effect\.

## 5Evaluation

The experiments test whether the LeanFlow workflow components in[Figure1](https://arxiv.org/html/2607.20503#S3.F1)improve real formalization and proving runs\. Each completed run reports task outcome, API calls, input tokens, and output tokens from the workflow logs; the released LeanFlow artifacts include the run configurations, prompts, and logs used for these tables\. All model\-backed runs use fixed decoding settings across conditions: temperature0\.30\.3, top\-p=0\.95p=0\.95, and a maximum output budget of 65,536 tokens per model turn\. We count only model API calls\. For GPT\-5\.5, one Codex CLI model turn is one call; for Kimi\-K2\.6, one request to the EPFL\-hosted inference endpoint is one call\. Terminal commands, file reads and edits, Lean/Lake invocations, LeanProbe checks, and other structured tool invocations are not counted as API calls\. For cost accounting, the GPT\-5\.5 runs used the Codex CLI under a US$200 GPT Pro subscription; one month of this subscription covered all GPT\-5\.5 experiments reported here\. The Kimi\-K2\.6 runs used a self\-hosted EPFL deployment on8×8\\timesH200 GPUs, and token\-cost estimates use CHF 0\.4802 per million input tokens and CHF 1\.4406 per million output tokens\. Because these two models use different accounting regimes, the tables report calls and tokens rather than converting all rows to a single monetary scale\.

### 5\.1Document\-Level Case Studies

The two document\-level case studies are selected for mathematical content and area diversity\. Frisch and Vaserstein’s Pythagorean\-polynomial paper\(Frisch and Vaserstein,[2007](https://arxiv.org/html/2607.20503#bib.bib6)\)requires formalizing the classicalT​\(a,b,c\)T\(a,b,c\)parametrization, parity and divisibility side conditions, the obstruction to a single integer\-coefficient polynomial triple, and the explicit four\-variable triple of integer\-valued rational polynomials\. Lyons and Zumbrun’s Cramer–Wold paper\(Lyons and Zumbrun,[2017](https://arxiv.org/html/2607.20503#bib.bib7)\)requires formalizing closed half\-spaces as measurable sets, equality of measures from matching half\-space values, the Crofton step from half\-space values to average\-distance functions, the odd\-dimensional Laplacian recovery argument, and the even\-to\-odd embeddingℝ2​m↪ℝ2​m\+1\\mathbb\{R\}^\{2m\}\\hookrightarrow\\mathbb\{R\}^\{2m\+1\}\.[AppendixA](https://arxiv.org/html/2607.20503#A1)gives the detailed source\-to\-Lean decomposition for both case studies\. To the best of our knowledge, neither source theorem had a prior proof\-assistant formalization\. The completed Pythagorean project comprises 83 Lean declarations \(34 of themtheorem/lemmastatements\) and the Cramer–Wold project 114 declarations \(101theorem/lemmastatements\); both build sorry\-free and free of unapproved axioms\.

For the workflow ablations reported in[Table3](https://arxiv.org/html/2607.20503#S5.T3), each source first runs through the pre\-proof stages in[Figures1](https://arxiv.org/html/2607.20503#S3.F1)and[1](https://arxiv.org/html/2607.20503#alg1): source resolution, blueprint construction, statement generation with proof placeholders, and statement/source review\. The result is a reviewed skeleton, i\.e\., a Lean statement layer that type\-checks with theorem bodies left as placeholders and has passed the source\-faithfulness checks in[Table1](https://arxiv.org/html/2607.20503#S4.T1)\. The Pythagorean reviewed skeleton is produced with Kimi\-K2\.6; the Cramer–Wold reviewed skeleton is produced with GPT\-5\.5 because the initial representation setup for probability measures, half\-spaces, and the analytic inversion target requires more representation choices than the Pythagorean source\. These pre\-proof stages are held fixed across the proof\-repair ablations, and the 2000\-call budget in[Table3](https://arxiv.org/html/2607.20503#S5.T3)begins after the reviewed skeleton has been accepted\. Statement translation, skeleton construction, the statement/source gate, and proof repair all run autonomously, with no human edits to the reviewed skeletons or to the proof runs in[Table3](https://arxiv.org/html/2607.20503#S5.T3); expert involvement is limited to verifying faithfulness after the fact \([Section6](https://arxiv.org/html/2607.20503#S6)\), because no automated faithfulness guarantee is currently available\.

### 5\.2Workflow Ablations on Real Sources

The primary evaluation is an ablation study: it compares the full LeanFlow against variants that remove the queue system and/or the specialized Lean tools\. For each model, we run the full2×22\\times 2design: queue versus no queue, and full tool surface versus terminal\-only interaction\.[Table3](https://arxiv.org/html/2607.20503#S5.T3)is organized by source so that completion behavior and model\-side budget can be compared within the same mathematical project\. Here and in later tables,*queue*means the two\-layer queue system: the project\-wide file queue plus the file\-scoped declaration queue\. All four conditions for a given source start from the same reviewed skeleton and use the same proof goal, prompt template, model settings, and call budget; only the queue system and tool surface are changed\. All document\-level proving runs have a maximum budget of 2000 prover\-agent API calls, where one call is one model turn in the proof\-repair loop\. In the terminal\-only condition, the agent may still read and edit files, search with shell tools such asrg, and run commands such aslake build, but it has no access to LeanProbe, MCP\-backed Lean tools, structured declaration search, or proof\-state APIs\. In the no\-queue condition, an outer runner still keeps the prover running until the project succeeds or the call budget expires, but both queue layers are disabled: the manager does not route files through a project queue, does not restrict the model to one top\-of\-queue declaration, and does not use theorem\-local failed\-attempt history to gate the next target\. Source preflight, the statement/source gate, final Lean/Lake verification, and hygiene checks are held fixed across conditions\.

Table 3:Long\-form workflow ablation on the two document\-level case studies\. Workflow abbreviations encode queue\-system and tool configuration: Full = both queue layers with full tools; NoQ\+Tools = no queue system with full tools; Q\+CLI = both queue layers with terminal\-only interaction; NoQ\+CLI = no queue system with terminal\-only interaction\. Outcome is*success*when the requested project builds underEEfrom the reviewed skeleton with no remainingsorryand no unapproved axioms within the 2000\-call budget, and*failure*otherwise\. Calls are prover\-agent API calls with a 2000\-call cap\.[Table3](https://arxiv.org/html/2607.20503#S5.T3)shows that the combined queue system is decisive for Kimi\-K2\.6 in these two document\-level runs: both no\-queue variants exhaust the 2000\-call budget on both case studies, while full LeanFlow succeeds in 1043 calls on Pythagorean triples and 1278 calls on Cramer–Wold\. The effect of the tool surface is most visible on the analytic case study, where Kimi\-K2\.6 with a queue but terminal\-only interaction still fails on Cramer–Wold\. For GPT\-5\.5, all document\-level variants succeed, so these rows do not establish LeanFlow as necessary for completion under this model\. Instead, they support an efficiency and auditability claim: full LeanFlow has the lowest or tied\-lowest input\-token cost on both sources, although the Cramer–Wold no\-queue/full\-tools run uses slightly fewer calls at a higher input\-token cost\.

### 5\.3RLM25\-PFR Autoformalization

We evaluate on RLM25\-PFR, the PFR slice of RLM25\(Poirouxet al\.,[2025a](https://arxiv.org/html/2607.20503#bib.bib17),[c](https://arxiv.org/html/2607.20503#bib.bib16)\), rather than on the full RLM25 benchmark\. This slice contains 145 theorem\-statement examples from the Polynomial Freiman–Ruzsa project\. We report it separately from the document\-to\-project case studies because each example is an independent theorem task rather than a complete source document\.

Each RLM25\-PFR example is run as a two\-stage Lean workflow with one shared 200\-call model budget per example\. First, the agent receives the informal statement, project context, and any available informal proof or blueprint material, and synthesizes a Lean declaration that must type\-check, typically with a placeholder proof\. The generated statement is evaluated against the reference formal statement using the benchmark’s BEq and BEq\+ statement\-equivalence metrics\. Second, the generated statement is treated as a fixed proof target: the prover may fill proof bodies and add local helper lemmas, but it may not weaken statements, introduce custom axioms, or leavesorry/admitplaceholders\. The call budget is shared by statement synthesis and proof completion, and the call totals in[Table4](https://arxiv.org/html/2607.20503#S5.T4)include both stages\. Runs are autonomous after launch, with no human edits to the generated statements or proofs\. If the 200\-call budget is exhausted before final verification, the example is counted as a proof failure\. Proof success requires final Lean/Lake verification and the same hygiene scan used in our document\-level runs\.[Table4](https://arxiv.org/html/2607.20503#S5.T4)summarizes the completed GPT\-5\.5 runs\. In this single GPT\-5\.5 run, LeanFlow reduces calls \(3,541 vs\. 4,053\) and input tokens \(203\.2M vs\. 236\.6M\) while increasing BEq\+ from 72\.9% to 75\.7%; because the runs lack variance estimates, we treat the BEq\+ change as a small effect rather than a significance claim\. The gap between proof success and statement\-equivalence metrics reinforces why verified proof completion cannot replace statement/source checks: a proved declaration can still formalize the wrong mathematical claim\.

To our knowledge, no published baseline reports provide proof\-of\-completion results for the RLM25\-PFR two\-stage setting; the original source\(Poirouxet al\.,[2025a](https://arxiv.org/html/2607.20503#bib.bib17)\)is not concerned with producing proofs of statements\.

Table 4:RLM25\-PFR agent\-run results on the PFR slice\. Proof success is the share of examples whose final Lean code verifies with no remaining placeholders or unapproved axioms under the 200\-call per\-example budget; BEq and BEq\+ are statement\-equivalence metrics against reference formal statements\. Calls and tokens are totals over the slice and include both statement synthesis and proof completion\.
### 5\.4Challenge Tasks

Project\-level proving tasks provide the formal statements and isolate proof construction\. The ICML 2026 AI for Math Track 2 TCS proving challenge tests project\-level algorithmic proof tasks in graph theory, combinatorics, computational complexity, and algorithm correctness using CSLib and a comparator\-backed pass\-rate metric\(AI for Math Workshop,[2026](https://arxiv.org/html/2607.20503#bib.bib5)\)\. The five challenge projects cover binary heap operations, a heap\-backed Dijkstra proof, Kruskal minimum spanning trees, segment\-tree construction and range queries, and treap invariant/runtime obligations\. Each run uses the same 2000\-call proof budget as the document\-level proof\-repair runs\. Success means that the final project passes the official SafeVerify/comparator check and also passes our local final Lean/Lake verification and hygiene scan with no remainingsorry/admitplaceholders or unapproved axioms\. We run all five projects with GPT\-5\.5 under three conditions: full LeanFlow, no queue system with LeanProbe still available, and no queue system with only terminal Lean/Lake interaction\. For Kimi\-K2\.6, we additionally run the Kruskal project with full LeanFlow and without either the queue system or the specialized tool surface\. All challenge runs are autonomous after launch, with no human edits to the proof files during the run\. The public Track 2 leaderboard lists our competition submission under thelmilikicidentifier at rank 2 in the combined Phase 1\+2 ranking\(AI for Math Workshop,[2026](https://arxiv.org/html/2607.20503#bib.bib5)\)\.

Table 5:AI4Math TCS challenge outcomes by project and workflow condition\. Workflow abbreviations encode queue\-system and tool configuration: Full = both queue layers with full tools; NoQ\+Probe = no queue system with LeanProbe available; NoQ\+CLI = no queue system with terminal\-only Lean/Lake interaction\. Calls are prover\-agent API calls with a 2000\-call per\-project cap\.[Table5](https://arxiv.org/html/2607.20503#S5.T5)shows that all GPT\-5\.5 variants solve all five TCS projects, so these rows do not isolate a single decisive workflow component\. The results are also consistent with LeanProbe being useful as a feedback surface: workflow logs show that GPT\-5\.5 used LeanProbe in 37% of recorded agent steps in TCS runs where the tool was available, and NoQ\+Probe uses fewer calls and lower input tokens than NoQ\+CLI on four of five projects\. This aligns with the tool design in[Section4\.6](https://arxiv.org/html/2607.20503#S4.SS6), where failed candidates can return local compiler diagnostics and proof\-state feedback before the next proof attempt\. For Kimi\-K2\.6, the tested Kruskal run succeeds with the full workflow, while the no\-queue terminal\-only variant reaches the 2000\-call budget\.

### 5\.5LeanProbe Utility

LeanProbe is evaluated separately because it changes verifier latency rather than model capability\. We compare cached LeanProbe checks against terminallake env leanchecks on two workloads that match the proof loop in[Figure2](https://arxiv.org/html/2607.20503#S4.F2)\. The repeated\-target workload measures many candidate replacements for one active declaration after a single prepare step\. The sequential workload measures a queue\-style file run: partial candidates are rejected against the current cached environment, while accepted declarations advance the environment for later targets\.

Table 6:LeanProbe latency benchmarks\. Repeated\-target times are average ranges in seconds after one prepare step; sequential rows report total seconds per compact file with five declarations and ten partial/full candidate scenarios\.[Table6](https://arxiv.org/html/2607.20503#S5.T6)supports the design choice of checking candidate edits frequently instead of waiting for large repair batches\. The prepare step is paid once before a target, and then each candidate proof replacement is checked in milliseconds to tens of milliseconds\. Sequential checks also match the queue design: the environment advances only after a complete declaration succeeds, so failed candidates are diagnosed without changing the context for later obligations\. The detailed LeanProbe experimental setup and per\-file results are reported in[AppendixB](https://arxiv.org/html/2607.20503#A2)\.

### 5\.6Statement\-Skeleton Case Study

We use a qualitative Pythagorean\-polynomial comparison to check whether the source\-to\-statement stages in[Algorithm1](https://arxiv.org/html/2607.20503#alg1)prevent statement drift before proof search\. The no\-review condition skips the blueprint and statement/source review stages in Steps 3 and 5: after seeing the source, the model is asked to produce Lean translations directly, without a recorded source\-to\-declaration map or an independent faithfulness check before proving\. The no\-review draft and the reviewed skeleton both build, but they formalize different mathematical objects\. The no\-review draft would support a less source\-faithful function\-level formalization of the result: it defines the main witnesses as rational\-valued functions on integer inputs\. The reviewed skeleton is the source\-faithful version under the checks in[Table1](https://arxiv.org/html/2607.20503#S4.T1): it defines the witnesses as rational multivariate polynomials and separately proves integer\-valuedness, matching the paper’s theorem\. The detailed declaration\-level contrast is reported in Appendix[A](https://arxiv.org/html/2607.20503#A1.SS0.SSS0.Px1)\([Table7](https://arxiv.org/html/2607.20503#A1.T7)\)\.

## 6Threats to Validity

The evaluation has several limitations\. Buildability is necessary but not sufficient: a project can build while encoding a different claim\. 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; reducing this manual confirmation is important future work\. The workflow also assumes that the source definitions and theorem statements are the targets to preserve\. After the statement/source gate accepts a skeleton, the prover is not allowed to change definitions or theorem statements; this improves auditability, but it can make a proof obligation impossible if the source contains a typo, an omitted side condition, or an undetected mistranslation\. Such errors must be caught during statement/source review or expert audit rather than silently repaired during proof search\. The document\-level evidence covers only two case studies; the Cramer–Wold skeleton was initialized with GPT\-5\.5 rather than Kimi\-K2\.6 because of its representation choices\. The ablations are single runs, so they do not estimate variance; repeated document\-level runs would be more informative but costly, since each can require hundreds to thousands of calls, tens to hundreds of millions of input tokens, and substantial wall\-clock time\. Several mechanisms also remain bundled: queue/tool ablations do not isolate blueprinting, statement review, failed\-attempt memory, hygiene scanning, and LeanProbe feedback\. The complementary benchmarks do not fully exercise document\-to\-project formalization, the RLM25\-PFR rows cover only the PFR slice rather than the full RLM25 benchmark, the GPT\-5\.5 rows support efficiency claims more than necessity claims, and we do not include a matched document\-level M2F comparison\. Calls and token counts are useful proxies for model\-side effort, but not full measures of wall\-clock, monetary, or human engineering cost\.

## 7Conclusion

LeanFlow treats autoformalization as an evolving Lean project with durable workflow state, not as independent theorem prompts\. The central design choice is to keep project control outside the model: the runtime records source\-to\-Lean decisions, reviews statements before proof search, assigns proofs one at a time, checks candidate edits quickly, and accepts only builds that pass the verifier and contain no leftover placeholders or unapproved axioms\. The document\-level evidence is model\-dependent: in our two case studies, workflow control is decisive for Kimi\-K2\.6 completion under budget, while for GPT\-5\.5 it mainly improves token efficiency and audit discipline because every document\-level variant completes\.

## Impact Statement

This work aims to make Lean autoformalization more inspectable, reproducible, and verifier\-grounded\. Potential positive impacts include reducing the engineering burden of proof repair, improving the auditability of machine\-assisted formalization, and making document\-level formal verification workflows easier to study\. Potential risks include over\-reliance on generated formal artifacts, mistaking buildability for source faithfulness, and unequal access to the compute and model resources needed for long formalization runs\. LeanFlow is designed to mitigate these risks by recording source\-to\-Lean decisions, separating statement review from proof search, preserving workflow logs and checkpoints, and accepting final artifacts only after external Lean verification with no leftover placeholders or unapproved axioms\. The system is intended to assist expert formalizers rather than replace human mathematical judgment\.

## Author Contributions

Lazar Milikić led the system design, implementation, experiments, and paper writing\. Simon Guilloud helped with benchmarking code, research direction, and paper writing\. Khanh Nguyen contributed with research direction and paper writing\. Viktor Kunčak supervised the project, contributed to the research direction, and helped revise the manuscript\.

## Acknowledgments

This research is supported by the AI For Math Fund, administered by Renaissance Philanthropy and funded by XTX Markets\. We also gratefully acknowledge the support of the EPFL School of Computer and Communication Sciences\.

## References

- AI for Math Workshop \(2026\)ICML 2026 AI for math workshop track 2 leaderboard\.Note:[https://ai4math2026\.github\.io/track2/leaderboard/](https://ai4math2026.github.io/track2/leaderboard/)Track 2 theoretical computer science proving in Lean leaderboard and challenge scoring summaryCited by:[§1](https://arxiv.org/html/2607.20503#S1.p5.1),[§5\.4](https://arxiv.org/html/2607.20503#S5.SS4.p1.1)\.
- J\. Asher \(2025\)LeanExplore: a search engine for Lean 4 declarations\.External Links:2506\.11085,[Document](https://dx.doi.org/10.48550/arXiv.2506.11085),[Link](https://arxiv.org/abs/2506.11085)Cited by:[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px3.p1.1)\.
- Z\. Azerbayev, B\. Piotrowski, H\. W\. Schoelkopf, E\. W\. Ayers, D\. Radev, and J\. Avigad \(2023\)ProofNet: autoformalizing and formally proving undergraduate\-level mathematics\.External Links:2302\.12433,[Document](https://dx.doi.org/10.48550/arXiv.2302.12433),[Link](https://arxiv.org/abs/2302.12433)Cited by:[§1](https://arxiv.org/html/2607.20503#S1.p1.1),[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px1.p1.1)\.
- L\. de Moura and S\. Ullrich \(2021\)The Lean 4 theorem prover and programming language\.InAutomated Deduction – CADE 28,pp\. 625–635\.External Links:[Document](https://dx.doi.org/10.1007/978-3-030-79876-5%5F37)Cited by:[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px1.p1.1)\.
- S\. Frisch and L\. Vaserstein \(2007\)Parametrization of Pythagorean triples by a single triple of polynomials\.External Links:0706\.0290,[Link](https://arxiv.org/abs/0706.0290)Cited by:[§1](https://arxiv.org/html/2607.20503#S1.p6.1),[§5\.1](https://arxiv.org/html/2607.20503#S5.SS1.p1.2)\.
- F\. Gloeckle, A\. Rammal, C\. Arnal, R\. Munos, V\. Cabannes, G\. Synnaeve, and A\. Hayat \(2026\)Automatic textbook formalization\.External Links:2604\.03071,[Link](https://arxiv.org/abs/2604.03071)Cited by:[§1](https://arxiv.org/html/2607.20503#S1.p1.1),[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px2.p1.1)\.
- S\. Hariharan, C\. Birkbeck, S\. Lee, H\. K\. G\. Ma, B\. Mehta, A\. Poiroux, and M\. Viazovska \(2026\)A milestone in formalization: the sphere packing problem in dimension 8\.External Links:2604\.23468,[Link](https://arxiv.org/abs/2604.23468)Cited by:[§1](https://arxiv.org/html/2607.20503#S1.p1.1),[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px2.p1.1)\.
- A\. Letson, L\. Sarra, A\. Poiroux, O\. Dressler, P\. Lezeau, D\. Aranha, F\. Pu, A\. Hill, M\. C\. Hidalgo, J\. Berman, G\. Tsoukalas, and L\. Taelman \(2026\)SorryDB: can AI provers complete real\-world Lean theorems?\.External Links:2603\.02668,[Document](https://dx.doi.org/10.48550/arXiv.2603.02668),[Link](https://arxiv.org/abs/2603.02668)Cited by:[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px1.p1.1)\.
- J\. Lu, Y\. Wan, Z\. Liu, Y\. Huang, J\. Xiong, C\. Liu, J\. Shen, H\. Jin, J\. Zhang, H\. Wang, Z\. Yang, J\. Tang, and Z\. Guo \(2024\)Process\-driven autoformalization in Lean 4\.External Links:2406\.01940,[Document](https://dx.doi.org/10.48550/arXiv.2406.01940),[Link](https://arxiv.org/abs/2406.01940)Cited by:[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px2.p1.1)\.
- R\. Lyons and K\. Zumbrun \(2017\)A calculus proof of the Cramér–Wold theorem\.External Links:1607\.03206,[Link](https://arxiv.org/abs/1607.03206)Cited by:[§1](https://arxiv.org/html/2607.20503#S1.p6.1),[§5\.1](https://arxiv.org/html/2607.20503#S5.SS1.p1.2)\.
- Math, Inc\. \(2025\)Introducing Gauss, an agent for autoformalization\.Note:[https://www\.math\.inc/gauss](https://www.math.inc/gauss)Company announcementCited by:[§1](https://arxiv.org/html/2607.20503#S1.p1.1),[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px2.p1.1)\.
- Moonshot AI \(2026\)Kimi\-K2\.6: open\-weights native multimodal agentic model\.Note:[https://huggingface\.co/moonshotai/Kimi\-K2\.6](https://huggingface.co/moonshotai/Kimi-K2.6)Hugging Face model card formoonshotai/Kimi\-K2\.6Cited by:[§1](https://arxiv.org/html/2607.20503#S1.p3.1)\.
- A\. Poiroux, A\. Bosselut, and V\. Kuncak \(2025a\)RLMEval: evaluating research\-level neural theorem proving\.External Links:2510\.25427,[Document](https://dx.doi.org/10.48550/arXiv.2510.25427),[Link](https://arxiv.org/abs/2510.25427)Cited by:[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px2.p1.1),[§5\.3](https://arxiv.org/html/2607.20503#S5.SS3.p1.1),[§5\.3](https://arxiv.org/html/2607.20503#S5.SS3.p3.1)\.
- A\. Poiroux, V\. Kuncak, and A\. Bosselut \(2025b\)LeanInteract: a python interface for Lean 4\.Note:[https://github\.com/augustepoiroux/LeanInteract](https://github.com/augustepoiroux/LeanInteract)Cited by:[§1](https://arxiv.org/html/2607.20503#S1.p4.1),[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px3.p1.1),[§4\.6](https://arxiv.org/html/2607.20503#S4.SS6.p1.1)\.
- A\. Poiroux, G\. Weiss, V\. Kunčak, and A\. Bosselut \(2025c\)Reliable evaluation and benchmarks for statement autoformalization\.InProceedings of the 2025 Conference on Empirical Methods in Natural Language Processing,Suzhou, China,pp\. 17947–17969\.External Links:[Document](https://dx.doi.org/10.18653/v1/2025.emnlp-main.907),[Link](https://aclanthology.org/2025.emnlp-main.907/)Cited by:[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px2.p1.1),[§5\.3](https://arxiv.org/html/2607.20503#S5.SS3.p1.1)\.
- The mathlib Community \(2020\)The Lean mathematical library\.InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs,pp\. 367–381\.External Links:[Document](https://dx.doi.org/10.1145/3372885.3373824)Cited by:[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px1.p1.1)\.
- The PhysLib community \(2024\)PhysLib: the Lean physics library\.GitHub\.Note:[https://github\.com/leanprover\-community/physlib](https://github.com/leanprover-community/physlib)Formerly PhysLean/HepLeanCited by:[Appendix A](https://arxiv.org/html/2607.20503#A1.SS0.SSS0.Px2.p1.7)\.
- G\. Tsoukalas, A\. Kovsharov, S\. Shirobokov, A\. Surina, M\. Firsching, G\. Bérczi, F\. J\. R\. Ruiz, A\. Suggala, A\. Z\. Wagner, E\. Wieser, L\. Yu, A\. Huang, M\. Z\. Horváth, A\. Ferrauiolo, H\. Michalewski, C\. Grosu, T\. Hubert, M\. Balog, P\. Kohli, and S\. Chaudhuri \(2026\)Advancing mathematics research with ai\-driven formal proof search\.External Links:2605\.22763,[Link](https://arxiv.org/abs/2605.22763)Cited by:[§1](https://arxiv.org/html/2607.20503#S1.p1.1),[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px2.p1.1)\.
- G\. Tsoukalas, J\. Lee, J\. Jennings, J\. Xin, M\. Ding, M\. Jennings, A\. Thakur, and S\. Chaudhuri \(2024\)PutnamBench: evaluating neural theorem\-provers on the putnam mathematical competition\.External Links:2407\.11214,[Document](https://dx.doi.org/10.48550/arXiv.2407.11214),[Link](https://arxiv.org/abs/2407.11214)Cited by:[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px1.p1.1)\.
- Z\. Wang, W\. Ma, Z\. Ming, G\. Zhang, K\. Yuan, and Z\. Wen \(2026\)M2F: automated formalization of mathematical literature at scale\.External Links:2602\.17016,[Document](https://dx.doi.org/10.48550/arXiv.2602.17016),[Link](https://arxiv.org/abs/2602.17016)Cited by:[§1](https://arxiv.org/html/2607.20503#S1.p1.1),[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px2.p1.1)\.
- Y\. Wu, A\. Q\. Jiang, W\. Li, M\. N\. Rabe, C\. Staats, M\. Jamnik, and C\. Szegedy \(2022\)Autoformalization with large language models\.External Links:2205\.12615,[Document](https://dx.doi.org/10.48550/arXiv.2205.12615),[Link](https://arxiv.org/abs/2205.12615)Cited by:[§1](https://arxiv.org/html/2607.20503#S1.p1.1),[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px2.p1.1)\.
- Y\. Xin, Q\. Chen, G\. Durrett, and I\. Dillig \(2026\)VeriSoftBench: repository\-scale formal verification benchmarks for Lean\.External Links:2602\.18307,[Document](https://dx.doi.org/10.48550/arXiv.2602.18307),[Link](https://arxiv.org/abs/2602.18307)Cited by:[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px1.p1.1)\.
- K\. Yang, A\. M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. Anandkumar \(2023\)LeanDojo: theorem proving with retrieval\-augmented language models\.External Links:2306\.15626,[Document](https://dx.doi.org/10.48550/arXiv.2306.15626),[Link](https://arxiv.org/abs/2306.15626)Cited by:[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px3.p1.1)\.
- Z\. Yu, R\. Peng, K\. Ding, Y\. Li, Z\. Peng, M\. Liu, Y\. Zhang, Y\. Zheng, H\. Xin, W\. Huang, Y\. Wen, and W\. Liu \(2025\)FormalMATH: benchmarking formal mathematical reasoning of large language models\.External Links:2505\.02735,[Link](https://arxiv.org/abs/2505.02735)Cited by:[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px1.p1.1)\.
- K\. Zheng, J\. M\. Han, and S\. Polu \(2022\)MiniF2F: a cross\-system benchmark for formal olympiad\-level mathematics\.InInternational Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=9ZPegFuFTFv)Cited by:[§1](https://arxiv.org/html/2607.20503#S1.p1.1),[§2](https://arxiv.org/html/2607.20503#S2.SS0.SSS0.Px1.p1.1)\.

## Appendix ADocument Case Study Details

The LeanFlow implementation is available on GitHub at[epfl\-lara/LeanFlow](https://github.com/epfl-lara/LeanFlow), the LeanProbe verifier at[epfl\-lara/LeanProbe](https://github.com/epfl-lara/LeanProbe), and the generated formalization projects at[epfl\-lara/AutoformalizedProjects](https://github.com/epfl-lara/AutoformalizedProjects)\. Each released project is self\-contained and pins its own Lean toolchain and Mathlib revision \(for example, Leanv4\.30\.0\-rc2for the Pythagorean project andv4\.29\.1for Cramer–Wold\), so builds are reproducible without a single global environment\. The two case studies have also been contributed to the community[lean\-pool](https://github.com/Vilin97/lean-pool)repository of AI\-produced Lean developments \(pull requests[\#185](https://github.com/Vilin97/lean-pool/pull/185)and[\#186](https://github.com/Vilin97/lean-pool/pull/186)\)\.

#### Pythagorean\-polynomial source\.

The Frisch–Vaserstein source first defines Pythagorean triples, polynomial parametrization overℤ​\[x1,…,xn\]\\mathbb\{Z\}\[x\_\{1\},\\ldots,x\_\{n\}\], and integer\-valued parametrization overInt​\(ℤn\)⊆ℚ​\[x1,…,xn\]\\mathrm\{Int\}\(\\mathbb\{Z\}^\{n\}\)\\subseteq\\mathbb\{Q\}\[x\_\{1\},\\ldots,x\_\{n\}\]\. The formalization therefore introduces both integer\-coefficient and rational\-polynomial representations before stating the main claims\. The source\-level proof obligations are: the standard two\-family parametrization of triples, the obstruction to a single integer\-coefficient triple, the explicit four\-variable integer\-valued witness, the positive\-triple variant, and the four\-square unrestricted\-parameter variant\. The obstruction proof is algebraic: it uses the UFD structure ofℤ​\[x1,…,xn\]\\mathbb\{Z\}\[x\_\{1\},\\ldots,x\_\{n\}\], a gcd decomposition, parity facts, and the examples\(3,4,5\)\(3,4,5\)and\(4,3,5\)\(4,3,5\)to force a contradiction\. The construction proof uses the source map

T​\(a,b,c\)=\(c​\(a2−b2\)/2,c​a​b,c​\(a2\+b2\)/2\)T\(a,b,c\)=\\left\(c\(a^\{2\}\-b^\{2\}\)/2,\\;cab,\\;c\(a^\{2\}\+b^\{2\}\)/2\\right\)and the parity condition that makes all three coordinates integral\. The reviewed Lean layout separates these concerns into basic definitions, source handoff lemmas, obstruction lemmas, integer\-valued construction lemmas, positive\-triple lemmas, and explanatory material for cited background\. This layout also records source claims that are likely to be omitted in a proof\-only draft: the finite\-cover theorem for integer\-valued parametrizations, the displayed binomial\-polynomial identity, and the non\-UFD motivation forInt​\(ℤ\)\\mathrm\{Int\}\(\\mathbb\{Z\}\)\.

Table 7:Declaration\-level contrast in the Pythagorean statement skeleton\. The no\-review draft is generated directly from the source; the reviewed skeleton is the version accepted by the statement/source review conditions described in[Table1](https://arxiv.org/html/2607.20503#S4.T1)\.
#### Cramer–Wold source\.

The Lyons–Zumbrun source states that Borel probability measures onℝn\\mathbb\{R\}^\{n\}are determined by their values on closed half\-spaces\. The formalization representsℝn\\mathbb\{R\}^\{n\}as Lean Euclidean space, defines closed half\-spaces by a normal vector and threshold, and records half\-space value functions and the average\-distance function

fμ​\(y\)=∫\(‖y−x‖−‖x‖\)​𝑑μ​\(x\)\.f\_\{\\mu\}\(y\)=\\int\(\\\|y\-x\\\|\-\\\|x\\\|\)\\,d\\mu\(x\)\.The first analytic proof block packages the Crofton/Fubini argument showing that half\-space values determinefμf\_\{\\mu\}\. The second proof block packages the odd\-dimensional inversion step: after reindexing dimensions as2​m\+12m\+1, the needed kernel identity is that an\(m\+1\)\(m\+1\)\-fold Laplacian of the norm kernel recovers a nonzero multiple of the point mass at the origin\. In Lean\-facing terms, this requires a tempered\-distribution norm kernel, Fourier/Laplacian algebra for iterated Laplacians, transport between the Euclidean model used by PhysLib\(The PhysLib community,[2024](https://arxiv.org/html/2607.20503#bib.bib4)\)and the project’s odd\-dimensional space, and a bridge from PhysLib’s real distribution API to Mathlib’s complex tempered distributions\. The analytic formalization also produced reusable PhysLib infrastructure for distributional Laplacians of norm\-kernel fundamental solutions, contributed upstream in[leanprover\-community/physlib\#1175](https://github.com/leanprover-community/physlib/pull/1175)\. The even\-dimensional Cramer–Wold theorem is then reduced to the odd\-dimensional one by embeddingℝ2​m\\mathbb\{R\}^\{2m\}intoℝ2​m\+1\\mathbb\{R\}^\{2m\+1\}and transporting half\-space values along that embedding\. The reviewed skeleton keeps the Crofton and inversion blocks as named proof targets rather than folding them into the final theorem; this makes clear which missing analytic facts are mathematical infrastructure, not model\-generated assumptions\.

## Appendix BLeanProbe Benchmark Results

This appendix records the detailed LeanProbe benchmark rows behind[Table6](https://arxiv.org/html/2607.20503#S5.T6)\. The snapshot was refreshed on May 13, 2026, with Lean 4\.30\.0\-rc2\. These rows are verifier\-latency measurements, not model\-performance measurements: they isolate the cost of checking candidate Lean edits under different reuse policies\. The benchmark suite has two parts: grouped repeated\-target checks, which stress many alternatives for one active declaration, and sequential same\-file checks, which stress queue\-style advancement through a file\. All runs use one measured run per target/file, no benchmark warmups, warm Lake caches from prior validation, and a fresh\-server baseline\. LeanProbe remains a feedback surface; final file or project acceptance still uses standard Lean/Lake verification\.

#### Grouped repeated\-target benchmark\.

The repeated\-target workload measures the agent pattern of trying several complete replacements for one active declaration\. For each target, the benchmark writes a temporary full file and times terminallake env lean; then it starts LeanProbe, prepares the environment immediately before the target, checks the replacement against that cached environment, optionally requests proof\-state feedback, and finally repeats the check with a fresh LeanProbe/LeanInteract server to measure the no\-cache baseline\. The compact groups are Mathlib\-facing examples:analysis\_realcovers elementary real\-analysis facts,algebra\_ordercovers ordered algebra and inequalities,sets\_functionscovers set/function image and preimage reasoning, andnumber\_theory\_natcovers elementary natural\-number arithmetic\. The TCS groups are longer challenge\-style extracts:tcs\_binary\_heapcontains heap operations such asheapify,extract\_min,insert,merge, andremove;tcs\_treap\_analysiscontains the two probability\-sum obligations used in the treap analysis; andtcs\_weighted\_graphcontains weighted\-graph helper declarations through theSym2orderprefix\. In[Table8](https://arxiv.org/html/2607.20503#A2.T8),*Targets*is the number of active declarations in the group,*Lake full*is full\-file terminal verification,*Prepare*is the one\-time cached\-environment setup,*Cached*is a target replacement check after prepare,*Feedback*includes diagnostic/proof\-state metadata,*Fresh*is the same check with a fresh server, and*Fresh/cached*is the fresh\-check time divided by the cached\-check time\.

#### Sequential same\-file benchmark\.

The sequential workload models a queue\-managed file run rather than repeated attempts on one target\. Each compact file has five declarations and ten scenarios: for every targetable declaration, the benchmark checks a partial declaration containingsorryand then the complete declaration\. LeanProbe reports the partial scenario and detects thesorry, but it advances the cached environment only after the complete declaration succeeds\. The Lake baselines rerun terminal checks for every scenario, either on a growing prefix that includes accepted prior declarations or on a full temporary file in which only the current declaration is replaced\. In[Table9](https://arxiv.org/html/2607.20503#A2.T9),*Lake prefix*and*Lake full*are these two terminal baselines,*Probe cached*is one warm LeanProbe/LeanInteract server walking the whole file,*Probe fresh*restarts LeanProbe for every scenario, and the three speedup columns divide the corresponding baseline total by the cached LeanProbe total\.

Table 8:LeanProbe repeated\-target grouped results\. Times are averages in seconds; fresh/cached is the ratio between a fresh LeanProbe server and a cached check\.Table 9:LeanProbe sequential same\-file results\. Each file has five declarations and ten partial/full scenarios\. Times are total seconds for the file\.Repeated\-target rows isolate the cost of checking many replacements for one active declaration after a single prepare step\. Fornncomplete replacement attempts on the same target, the comparison is

Probe total​\(n\)=Prepare\+n⋅Cached,Lake total​\(n\)=n⋅Lake full\.\\text\{Probe total\}\(n\)=\\text\{Prepare\}\+n\\cdot\\text\{Cached\},\\qquad\\text\{Lake total\}\(n\)=n\\cdot\\text\{Lake full\}\.The preparation cost is therefore amortized as soon as a target receives several candidate repairs: after setup, each additional candidate costs the cached\-check time instead of another full\-filelake env leanrun\. The grouped rows report this steady\-state behavior directly through*Cached*,*Fresh*, and*Fresh/cached*; the sequential rows report the end\-to\-end cost when successful declarations advance the environment\. Sequential rows model queue\-style proving in one file: partialsorryscenarios are diagnosed but not cached, while complete accepted declarations advance the environment for later targets\. This matches the proof\-loop policy used in our runs: keep the LeanProbe server warm, prepare once before a target when several repairs are likely, and advance the cached environment only after a complete declaration has been accepted\.