LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization

Khanh Nguyen; Lazar Milikic; Simon Guilloud; Viktor Kuncak

REVIEW 4 major objections 5 minor 30 references

LeanFlow claims that moving workflow control outside the LLM—a two-layer queue plus a statement/source gate—lets document-level autoformalization finish under budget where unmanaged runs fail.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-02 09:47 UTC pith:3Y6E4P24

load-bearing objection A clearly-written, honestly-scoped systems case study; the workflow design is useful, but the queue-decisive claim rests on n=1 runs and an unvalidated statement gate, so treat the numbers as preliminary. the 4 major comments →

arxiv 2607.20503 v1 pith:3Y6E4P24 submitted 2026-06-26 cs.AI cs.LGcs.LO

LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization

Lazar Milikic , Simon Guilloud , Khanh Nguyen , Viktor Kuncak This is my paper

classification cs.AI cs.LGcs.LO

keywords autoformalizationLean 4LLM agentsworkflow controlstatement faithfulnessproof repairverifier-in-the-loopdocument formalization

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper claims that in document-scale autoformalization—turning a whole mathematical paper into a buildable Lean project—the runtime structure, not just the underlying model, determines whether the job finishes on budget. The authors build LeanFlow, which keeps workflow control outside the model: a deterministic preflight, a blueprint mapping source spans to planned Lean declarations, a statement/source gate that reviews formal statements for faithfulness before proof search, and a two-layer prover queue that assigns one declaration at a time. In ablations on two previously unformalized papers, the full workflow lets one model (Kimi-K2.6) complete both projects within a 2000-call budget (1043 and 1278 calls), while every no-queue variant exhausts the budget; with a second model (GPT-5.5), all variants complete, and the full workflow has the lowest or tied-lowest input-token cost on both sources. A cached same-file verifier, LeanProbe, makes the per-declaration loop affordable by checking candidate edits roughly 9–14× faster than rerunning growing-prefix build checks. The upshot is a model-dependent but replicable argument that queue control, source-faithfulness review, and fast repair feedback are the load-bearing mechanisms for document-to-project formalization.

Core claim

The central discovery is that the two-layer queue system is decisive for completion under budget in the document-level runs: with Kimi-K2.6, the full LeanFlow workflow succeeds on the Pythagorean-triples paper in 1043 prover calls and on the Cramer–Wold paper in 1278 calls, whereas both no-queue variants (with and without the full tool surface) exhaust the 2000-call cap on both sources. For GPT-5.5 every document-level variant succeeds, so the workflow is not necessary for completion for that model; instead the full workflow delivers the lowest or tied-lowest input-token cost on both sources, and the run logs preserve an audit trail. The paper further shows that type-checking alone does not

What carries the argument

The load-bearing mechanism is the separation of mathematical editing from workflow control. A deterministic preflight resolves the source document and builds a blueprint—a project-local source map tying each planned Lean declaration to source spans, dependencies, and proof notes. A statement/source gate, a fresh LLM reviewer context with no human in the loop, then checks the generated skeleton against the source for drift (statement type, quantifiers, variable types, hypotheses, conclusion, encoding bridges, hygiene) before any proof search. The prover is governed by a two-layer queue: a project-wide file queue that ranks files by dependency, and a file-scoped declaration queue that exposes

Load-bearing premise

The statement/source gate—a single fresh LLM reviewer invocation with no human in the loop—can reliably tell whether a well-typed Lean declaration says the same thing as the source prose; the paper itself concedes there is currently no automated way to guarantee this and confirms faithfulness by expert inspection after the fact.

What would settle it

Take the two reviewed skeletons and deliberately introduce statement drift one declaration at a time—weaken an equality to an implication, change a domain from integers to naturals, swap quantifier order—then run the statement/source gate on each drifted version. If a non-negligible share of drifted declarations passes the gate, the faithfulness guarantee that underwrites the auditability claim is not met. Alternatively, run the full workflow with the gate's approval inverted (approve everything) on the two case studies: if expert inspection still finds the completed projects faithful and they

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

Document-level formalization can be completed under a fixed call budget when the runtime, not the model, decides which theorem to attempt next; for Kimi-K2.6, removing the queue turns success (1043–1278 calls) into budget exhaustion (2000 calls).
For a stronger model (GPT-5.5), the queue does not change completion—all variants succeed—but it cuts input-token cost, so workflow control is worth adopting for efficiency and auditability even when not strictly necessary.
Type-checking a declaration is not enough to guarantee faithfulness: the no-review draft and the reviewed skeleton both build but formalize different mathematical objects, so an independent statement/source gate is needed before proof search.
Cached verification (LeanProbe) makes a single-obligation loop affordable: sequential same-file checks run roughly 9–14× faster than growing-prefix build checks, which is what lets the queue loop retry quickly.
The completed Pythagorean and Cramer–Wold projects (83 and 114 declarations) build with no remaining placeholders and no unapproved axioms, and both were contributed to a community collection of AI-produced formalizations.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Editorial inference: because the ablations bundle blueprint review, queue memory, hygiene scanning, and LeanProbe into 'full workflow,' the paper does not isolate which sub-mechanism is decisive if the queue is the gate. A natural next ablation is to run the no-queue condition with only the statement/source gate added, to separate gating from ordering effects.
Editorial inference: a testable extension is that on longer documents the dependency-churn argument predicts unmanaged runs should degrade superlinearly in call budget relative to queue-managed runs, since failed edits can destabilize later declarations; a multi-chapter formalization would put that prediction under stress.
Editorial inference: the gate's reliability could be measured directly by starting from a set of source statements, automatically applying known drift mutations (weakened conclusions, swapped quantifiers, changed domains), and running the gate; the rejection rate on those mutations is a concrete audit of the faithfulness claim.
Editorial inference: the after-the-fact expert inspection that the paper concedes could be folded into the loop—a hybrid gate that flags low-confidence declarations for human review would make the auditability claim more robust without relying on a single autonomous reviewer.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Desk Editor's Note

A clearly-written, honestly-scoped systems case study; the workflow design is useful, but the queue-decisive claim rests on n=1 runs and an unvalidated statement gate, so treat the numbers as preliminary.

read the letter

Short version: LeanFlow is a solid piece of workflow engineering with a genuinely useful design, and it's refreshingly honest about its own limits. The thing to know before citing the 'decisive' claim is that the queue effect for Kimi-K2.6 comes from exactly one successful run per condition — no variance — and the statement/source gate, the component that keeps the prover from proving the wrong theorem, has no measured accuracy. The completion numbers in Table 3 are existence proofs, not robust effect sizes.

What's new and what works: the two-layer queue (project-wide file queue plus file-scoped declaration queue), the statement/source gate before proof search, and the cached LeanProbe verifier form a combination I haven't seen in the cited prior work. The two formalizations (Frisch–Vaserstein and Lyons–Zumbrun) are claimed firsts, and the projects are released with pinned toolchains and contributed to lean-pool. The LeanProbe latency measurements are concrete and reproducible — 9–14× speedup over growing-prefix Lake checks is real. The paper also openly concedes the big limitations: single runs, bundled mechanisms, no M2F comparison, no automated faithfulness guarantee. That's credit-worthy.

The soft spots, in proportion: the statement/source gate is a single fresh LLM review invocation with no false-accept rate, no precision/recall, no stress test. Section 6 concedes expert inspection after the fact. This matters because every success in Table 3 is a proof of a declaration this gate approved. If the gate misses drift, the build certifies the wrong statement. The RLM25-PFR drift (BEq+ < 100%) shows the risk is concrete. It doesn't sink the paper — the qualitative example in Table 7 shows the gate catching a real drift — but it means the document-to-project claim is only as strong as this unmeasured heuristic. Second, the ablations are single runs; we have no idea if the Kimi no-queue failures are stable or near-threshold. Third, the Cramer–Wold skeleton was made with GPT-5.5 and then used for Kimi ablation rows; the skeleton is fixed across conditions, so it's not a confound for the ablation, but it does limit what those rows say about the whole pipeline for Kimi. Fourth, the RLM25-PFR benchmark involves a coauthor, and the BEq+ gain is small and treated as small — fine, but don't over-read it.

Who gets value: anyone working on document-scale autoformalization, LLM agents for Lean, or benchmark design for formalization. It deserves a serious referee — the design is real and the artifacts are there — but the referee should ask for repeated runs (or at least variance estimates) and a gate-accuracy evaluation, even a small labeled set, before the completion claims are accepted as robust. My recommendation: send it to review, expect revision.

Referee Report

4 major / 5 minor

Summary. LeanFlow is an LLM-agent runtime for translating complete mathematical papers into buildable Lean projects. The system separates source preflight, blueprint construction, a statement/source faithfulness gate, a project-wide and file-scoped prover queue, and a cached verifier (LeanProbe). The paper reports document-level ablations on two previously unformalized papers — Frisch–Vaserstein on Pythagorean triples and Lyons–Zumbrun on Cramer–Wold — with Kimi-K2.6 and GPT-5.5, together with RLM25-PFR and ICML 2026 AI4Math TCS challenge runs. The main claims are that the queue system is decisive for Kimi-K2.6 completion under a 2000-call budget, that for GPT-5.5 the full workflow improves token efficiency, and that LeanProbe gives large latency speedups. The paper is candid about several limitations: single runs with no variance estimates, an unvalidated statement/source gate, and expert confirmation of faithfulness only after the fact.

Significance. If the central claims hold, the paper is a useful contribution to document-to-project autoformalization: it isolates workflow mechanisms rather than presenting another end-to-end system, releases the implementation and generated projects, pins Lean/Mathlib revisions, and separates statement faithfulness from proof completion. The latency measurements for cached verification are concrete and reproducible. However, the evidence is preliminary in important respects: the central completion comparison rests on single runs, the statement/source gate has no measured accuracy, and the two model rows are not fully symmetric because one skeleton was produced by the other model. The paper's explicit and repeated acknowledgment of these limitations is a strength, but the limitations currently prevent the stronger claims from being fully supported.

major comments (4)

[§4.3, §5.6, §6; Table 3] The statement/source gate is load-bearing for every completion in Table 3, yet no accuracy evaluation is reported. The gate is a single fresh LLM invocation (Sec. 4.3); the only evidence is one qualitative contrast (Table 7) showing a rejection, and Sec. 6 concedes that there is no automated guarantee of faithfulness, with expert inspection only after the fact. A false accept would make a 'successful' run certify a different theorem, so the queue/tool conclusions are conditional on unmeasured gate accuracy. Please report gate agreement rates on the two skeletons, ideally against independent human audit, and state how many reviewed declarations were subsequently confirmed faithful.
[§5.2, Table 3; §6] The central Kimi-K2.6 comparison rests on one run per condition, with no variance estimates; the paper acknowledges this in Sec. 6, but the decisive claim that the queue system is needed for completion is a single-run observation. In addition, the Cramer–Wold reviewed skeleton was produced with GPT-5.5 (Sec. 5.1), while the Pythagorean skeleton was produced with Kimi-K2.6. Thus each model is ablated on a statement layer that was, for one of the two sources, created by the other model. This confounds model-specific claims about queue benefit. Please add repeated runs at least at the success/failure boundary, or temper the claims, and state the skeleton-generating model for each row.
[§5.2, Table 3] The no-queue conditions are described as still having an 'outer runner' that keeps the prover running until the project succeeds or the budget expires. This runner may preserve some project-level control that is not part of the two-layer queue system being ablated. The paper should specify exactly what the no-queue runner does and does not do — e.g., whether it restarts, caches, or performs any global bookkeeping. Without this, the 'queue vs no queue' comparison is not a pure test of the two-layer queue manager.
[§5.3, Table 4] The RLM25-PFR results are from a single GPT-5.5 run, and the paper itself treats the BEq+ improvement as a small effect. More importantly, proof success (81.2%) and BEq+ (75.7%) are reported on the same slice, but the paper does not report the intersection: how many examples that were proved also had BEq+-equivalent statements. Since the paper argues that a proved declaration can formalize the wrong claim, this intersection is the relevant metric for the two-stage workflow. Please report it, or state explicitly that it is unavailable.

minor comments (5)

[Abstract / main text] The abstract uses 'Kimi2.6' and 'GPT5.5' without hyphens, while the main text uses 'Kimi-K2.6' and 'GPT-5.5'. Please use consistent model names throughout.
[Table 6 / Appendix B] In the repeated-target rows, the one-time prepare step can exceed a full-file Lake check (e.g., macOS 'analysis real': prepare 6.024s vs Lake full 3.893s). This is likely startup overhead, but the text should explicitly explain why prepare is sometimes slower than the full-file baseline and how the amortization argument is affected.
[§3] The final project gate is defined as a build plus a hygiene scan, but the paper does not state whether the hygiene scan is fully automated or partly manual. Please clarify, since 'no unapproved sorry/axiom' is a central acceptance criterion.
[§5.1] The sentence 'To the best of our knowledge, neither source theorem had a prior proof-assistant formalization' would benefit from a brief explanation of how this was checked, or from a citation to a searchable repository rather than leaving it as an assertion.
[Figure 1] Figure 1 is dense and labels several stages (preflight, blueprint, statement/source gate, queue, LeanProbe, final gates). Consider adding a small annotated arrow for the no-review ablation path used in Sec. 5.6, since that ablation skips blueprint and gate stages and is otherwise easy to misread.

Circularity Check

0 steps flagged

No circular derivation: claims are empirical, verifier-grounded, and controlled by ablations.

full rationale

LeanFlow is a systems/empirical paper. Its central claims — that the queue system affects completion for Kimi-K2.6 and token efficiency for GPT-5.5, and that LeanProbe reduces verifier latency — are measured outcomes from controlled ablations, not derived quantities. Acceptance criteria are external to the system: standard Lean/Lake verification, sorry/axiom hygiene scans, and the official TCS challenge comparator. Success is therefore not defined by the paper's own outputs or fitted parameters. The RLM25-PFR calibration uses a benchmark and BEq/BEq+ metrics from prior work by one of the present authors, but this self-citation is not load-bearing: it is explicitly presented as complementary calibration, and the document-level conclusions do not depend on it. Section 6 candidly lists limitations (no automated faithfulness guarantee, single runs, bundled mechanisms), which are validity threats rather than circular steps. No equation or parameter is fitted and later reported as a prediction; no uniqueness theorem or ansatz is imported from a self-citation to force a conclusion. There is no specific reduction of a claimed result to its inputs by construction.

Axiom & Free-Parameter Ledger

3 free parameters · 3 axioms · 0 invented entities

No new mathematical or physical entities are introduced; LeanFlow and LeanProbe are software systems, not postulated entities with independent falsifiable handles.

free parameters (3)

prover call budget cap = 2000 calls per document-level project
All document-level ablations cap at 2000 prover-agent API calls; the headline result that no-queue variants 'exhaust the budget' is relative to this chosen cap, and a larger budget could change outcomes.
per-example RLM25 budget = 200 calls
Proof success rate on RLM25-PFR is measured under a shared 200-call per-example budget; results depend on this cap.
decoding settings = temperature 0.3, top-p 0.95, max output 65536 tokens
Fixed across conditions, chosen by the authors; not fitted to data but could influence all model behavior.

axioms (3)

domain assumption Buildability plus hygiene scan (no sorry/admit/unsafe/axioms) is used as the success criterion for formalization.
Section 3 final gates; the paper itself notes in Section 6 that 'Buildability is necessary but not sufficient: a project can build while encoding a different claim.'
domain assumption The statement/source gate's LLM reviewer reliably detects statement drift without a human in the loop.
Section 4.3; Section 6 concedes no automated faithfulness guarantee exists and expert inspection is still required.
domain assumption The two reviewed skeletons correctly represent the source mathematics before proof repair.
Section 5.1: reviewed skeletons are 'held fixed across the proof-repair ablations'; if a skeleton mistranslates the source, downstream proof completion formalizes the wrong claim.

pith-pipeline@v1.3.0-alltime-deepseek · 15857 in / 10185 out tokens · 90748 ms · 2026-08-02T09:47:21.532818+00:00 · methodology

0 comments

read the original 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 Kimi2.6 and GPT5.5; we report task outcome, API calls, input tokens, and output tokens. With Kimi2.6, the full workflow completes both document-level projects within the 2000-call budget, while no-queue variants reach the budget limit; with GPT5.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 GPT5.5 runs.

Figures

Figures reproduced from arXiv: 2607.20503 by Khanh Nguyen, Lazar Milikic, Simon Guilloud, Viktor Kuncak.

**Figure 1.** 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… view at source ↗

**Figure 2.** Figure 2: File-scoped proving loop. Failed checks update theoremlocal memory; accepted edits advance to file/Lake verification sweeps. LeanProbe feedback on a failed candidate theorem add comm candidate (x y : Nat) : x + y = y + x := by /- <feedback> -- proof state: x y : Nat ⊢ x + y = y + x </feedback> -/ rfl /- <feedback> -- error: tactic ’rfl’ failed </feedback> -/ [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

**Figure 3.** 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.6. LeanProbe 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 LeanIn… view at source ↗

discussion (0)

Reference graph

Works this paper leans on

30 extracted references · 2 canonical work pages

[1]

doi:10.48550/arXiv.2602.17016 , url =

Wang, Zichen and Ma, Wanli and Ming, Zhenyu and Zhang, Gong and Yuan, Kun and Wen, Zaiwen , year =. doi:10.48550/arXiv.2602.17016 , url =. 2602.17016 , archivePrefix =

doi:10.48550/arxiv.2602.17016
[2]

Poiroux, Auguste and Kuncak, Viktor and Bosselut, Antoine , year =
[3]

2026 , howpublished =

2026
[4]

2024 , publisher =

GitHub repository , howpublished =. 2024 , publisher =

2024
[5]

Parametrization of

Frisch, Sophie and Vaserstein, Leonid , year =. Parametrization of. 0706.0290 , archivePrefix =

Pith/arXiv arXiv
[6]

A Calculus Proof of the

Lyons, Russell and Zumbrun, Kevin , year =. A Calculus Proof of the. 1607.03206 , archivePrefix =

Pith/arXiv arXiv
[7]

de Moura, Leonardo and Ullrich, Sebastian , booktitle =. The. 2021 , publisher =

2021
[8]

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , pages =

The. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , pages =. 2020 , publisher =

2020
[9]

2022 , url =

Zheng, Kunhao and Han, Jesse Michael and Polu, Stanislas , booktitle =. 2022 , url =

2022
[10]

and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima , year =

Yang, Kaiyu and Swope, Aidan M. and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima , year =. doi:10.48550/arXiv.2306.15626 , url =. 2306.15626 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2306.15626
[11]

doi:10.48550/arXiv.2506.11085 , url =

Asher, Justin , year =. doi:10.48550/arXiv.2506.11085 , url =. 2506.11085 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2506.11085
[12]

2022 , eprint =

Autoformalization with Large Language Models , author =. 2022 , eprint =. doi:10.48550/arXiv.2205.12615 , url =

Pith/arXiv arXiv doi:10.48550/arxiv.2205.12615 2022
[13]

and Ayers, Edward W

Azerbayev, Zhangir and Piotrowski, Bartosz and Schoelkopf, Hailey W. and Ayers, Edward W. and Radev, Dragomir and Avigad, Jeremy , year =. doi:10.48550/arXiv.2302.12433 , url =. 2302.12433 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2302.12433
[14]

Process-Driven Autoformalization in

Lu, Jianqiao and Wan, Yingjia and Liu, Zhengying and Huang, Yinya and Xiong, Jing and Liu, Chengwu and Shen, Jianhao and Jin, Hui and Zhang, Jipeng and Wang, Haiming and Yang, Zhicheng and Tang, Jing and Guo, Zhijiang , year =. Process-Driven Autoformalization in. doi:10.48550/arXiv.2406.01940 , url =. 2406.01940 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2406.01940
[15]

Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing , pages =

Reliable Evaluation and Benchmarks for Statement Autoformalization , author =. Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing , pages =. 2025 , address =. doi:10.18653/v1/2025.emnlp-main.907 , url =

work page doi:10.18653/v1/2025.emnlp-main.907 2025
[16]

doi:10.48550/arXiv.2510.25427 , url =

Poiroux, Auguste and Bosselut, Antoine and Kuncak, Viktor , year =. doi:10.48550/arXiv.2510.25427 , url =. 2510.25427 , archivePrefix =

doi:10.48550/arxiv.2510.25427
[17]

Gehrunger, Tim and Dekoninck, Jasper and Vechev, Martin , year =
[18]

2025 , howpublished =

Introducing. 2025 , howpublished =

2025
[19]

Taylor, Alexander K. and Zhang, Junyi and Ji, Ethan and Sahai, Vigyan and Deng, Haikang and Chen, Yuanzhou and Yuan, Yifan and Wu, Di and Gu, Jia-Chen and Chang, Kai-Wei and Peng, Nanyun and Sahai, Amit and Wang, Wei , year =. doi:10.48550/arXiv.2603.12744 , url =. 2603.12744 , archivePrefix =

doi:10.48550/arxiv.2603.12744
[20]

doi:10.48550/arXiv.2408.03350 , url =

Hu, Jiewen and Zhu, Thomas and Welleck, Sean , year =. doi:10.48550/arXiv.2408.03350 , url =. 2408.03350 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2408.03350
[21]

Construction-Verification: A Benchmark for Applied Mathematics in

Yang, Bowen and Yuan, Yi and Li, Chenyi and Wang, Ziyu and Li, Liangqi and Zhang, Bo and Li, Zhe and Wen, Zaiwen , year =. Construction-Verification: A Benchmark for Applied Mathematics in. doi:10.48550/arXiv.2602.01291 , url =. 2602.01291 , archivePrefix =

work page doi:10.48550/arxiv.2602.01291
[22]

doi:10.48550/arXiv.2603.02668 , url =

Letson, Austin and Sarra, Leopoldo and Poiroux, Auguste and Dressler, Oliver and Lezeau, Paul and Aranha, Dhyan and Pu, Frederick and Hill, Aaron and Hidalgo, Miguel Corredera and Berman, Julian and Tsoukalas, George and Taelman, Lenny , year =. doi:10.48550/arXiv.2603.02668 , url =. 2603.02668 , archivePrefix =

doi:10.48550/arxiv.2603.02668
[23]

doi:10.48550/arXiv.2602.18307 , url =

Xin, Yutong and Chen, Qiaochu and Durrett, Greg and Dillig, Isil , year =. doi:10.48550/arXiv.2602.18307 , url =. 2602.18307 , archivePrefix =

doi:10.48550/arxiv.2602.18307
[24]

doi:10.48550/arXiv.2510.02335 , url =

Yang, Xiao-Wen and Zhang, Zihao and Cao, Jianuo and Zhou, Zhi and Li, Zenan and Guo, Lan-Zhe and Yao, Yuan and Chen, Taolue and Li, Yu-Feng and Ma, Xiaoxing , year =. doi:10.48550/arXiv.2510.02335 , url =. 2510.02335 , archivePrefix =

doi:10.48550/arxiv.2510.02335
[25]

2505.02735 , archivePrefix =

Yu, Zhouliang and Peng, Ruotian and Ding, Keyi and Li, Yizhe and Peng, Zhongyuan and Liu, Minghao and Zhang, Yifan and Zheng, Yuan and Xin, Huajian and Huang, Wenhao and Wen, Yandong and Liu, Weiyang , year =. 2505.02735 , archivePrefix =

Pith/arXiv arXiv
[26]

doi:10.48550/arXiv.2407.11214 , url =

Tsoukalas, George and Lee, Jasper and Jennings, John and Xin, Jimmy and Ding, Michelle and Jennings, Michael and Thakur, Amitayush and Chaudhuri, Swarat , year =. doi:10.48550/arXiv.2407.11214 , url =. 2407.11214 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2407.11214
[27]

Ren, Z. Z. and Shao, Zhihong and Song, Junxiao and Xin, Huajian and Wang, Haocheng and Zhao, Wanjia and Zhang, Liyue and Fu, Zhe and Zhu, Qihao and Yang, Dejian and Wu, Z. F. and Gou, Zhibin and Ma, Shirong and Tang, Hongxuan and Liu, Yuxuan and Gao, Wenjun and Guo, Daya and Ruan, Chong , year =. doi:10.48550/arXiv.2504.21801 , url =. 2504.21801 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2504.21801
[28]

2026 , eprint=

Automatic Textbook Formalization , author=. 2026 , eprint=

2026
[29]

2026 , eprint=

Advancing Mathematics Research with AI-Driven Formal Proof Search , author=. 2026 , eprint=

2026
[30]

2026 , eprint=

A Milestone in Formalization: The Sphere Packing Problem in Dimension 8 , author=. 2026 , eprint=

2026

[1] [1]

doi:10.48550/arXiv.2602.17016 , url =

Wang, Zichen and Ma, Wanli and Ming, Zhenyu and Zhang, Gong and Yuan, Kun and Wen, Zaiwen , year =. doi:10.48550/arXiv.2602.17016 , url =. 2602.17016 , archivePrefix =

doi:10.48550/arxiv.2602.17016

[2] [2]

Poiroux, Auguste and Kuncak, Viktor and Bosselut, Antoine , year =

[3] [3]

2026 , howpublished =

2026

[4] [4]

2024 , publisher =

GitHub repository , howpublished =. 2024 , publisher =

2024

[5] [5]

Parametrization of

Frisch, Sophie and Vaserstein, Leonid , year =. Parametrization of. 0706.0290 , archivePrefix =

Pith/arXiv arXiv

[6] [6]

A Calculus Proof of the

Lyons, Russell and Zumbrun, Kevin , year =. A Calculus Proof of the. 1607.03206 , archivePrefix =

Pith/arXiv arXiv

[7] [7]

de Moura, Leonardo and Ullrich, Sebastian , booktitle =. The. 2021 , publisher =

2021

[8] [8]

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , pages =

The. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , pages =. 2020 , publisher =

2020

[9] [9]

2022 , url =

Zheng, Kunhao and Han, Jesse Michael and Polu, Stanislas , booktitle =. 2022 , url =

2022

[10] [10]

and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima , year =

Yang, Kaiyu and Swope, Aidan M. and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima , year =. doi:10.48550/arXiv.2306.15626 , url =. 2306.15626 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2306.15626

[11] [11]

doi:10.48550/arXiv.2506.11085 , url =

Asher, Justin , year =. doi:10.48550/arXiv.2506.11085 , url =. 2506.11085 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2506.11085

[12] [12]

2022 , eprint =

Autoformalization with Large Language Models , author =. 2022 , eprint =. doi:10.48550/arXiv.2205.12615 , url =

Pith/arXiv arXiv doi:10.48550/arxiv.2205.12615 2022

[13] [13]

and Ayers, Edward W

Azerbayev, Zhangir and Piotrowski, Bartosz and Schoelkopf, Hailey W. and Ayers, Edward W. and Radev, Dragomir and Avigad, Jeremy , year =. doi:10.48550/arXiv.2302.12433 , url =. 2302.12433 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2302.12433

[14] [14]

Process-Driven Autoformalization in

Lu, Jianqiao and Wan, Yingjia and Liu, Zhengying and Huang, Yinya and Xiong, Jing and Liu, Chengwu and Shen, Jianhao and Jin, Hui and Zhang, Jipeng and Wang, Haiming and Yang, Zhicheng and Tang, Jing and Guo, Zhijiang , year =. Process-Driven Autoformalization in. doi:10.48550/arXiv.2406.01940 , url =. 2406.01940 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2406.01940

[15] [15]

Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing , pages =

Reliable Evaluation and Benchmarks for Statement Autoformalization , author =. Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing , pages =. 2025 , address =. doi:10.18653/v1/2025.emnlp-main.907 , url =

work page doi:10.18653/v1/2025.emnlp-main.907 2025

[16] [16]

doi:10.48550/arXiv.2510.25427 , url =

Poiroux, Auguste and Bosselut, Antoine and Kuncak, Viktor , year =. doi:10.48550/arXiv.2510.25427 , url =. 2510.25427 , archivePrefix =

doi:10.48550/arxiv.2510.25427

[17] [17]

Gehrunger, Tim and Dekoninck, Jasper and Vechev, Martin , year =

[18] [18]

2025 , howpublished =

Introducing. 2025 , howpublished =

2025

[19] [19]

Taylor, Alexander K. and Zhang, Junyi and Ji, Ethan and Sahai, Vigyan and Deng, Haikang and Chen, Yuanzhou and Yuan, Yifan and Wu, Di and Gu, Jia-Chen and Chang, Kai-Wei and Peng, Nanyun and Sahai, Amit and Wang, Wei , year =. doi:10.48550/arXiv.2603.12744 , url =. 2603.12744 , archivePrefix =

doi:10.48550/arxiv.2603.12744

[20] [20]

doi:10.48550/arXiv.2408.03350 , url =

Hu, Jiewen and Zhu, Thomas and Welleck, Sean , year =. doi:10.48550/arXiv.2408.03350 , url =. 2408.03350 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2408.03350

[21] [21]

Construction-Verification: A Benchmark for Applied Mathematics in

Yang, Bowen and Yuan, Yi and Li, Chenyi and Wang, Ziyu and Li, Liangqi and Zhang, Bo and Li, Zhe and Wen, Zaiwen , year =. Construction-Verification: A Benchmark for Applied Mathematics in. doi:10.48550/arXiv.2602.01291 , url =. 2602.01291 , archivePrefix =

work page doi:10.48550/arxiv.2602.01291

[22] [22]

doi:10.48550/arXiv.2603.02668 , url =

Letson, Austin and Sarra, Leopoldo and Poiroux, Auguste and Dressler, Oliver and Lezeau, Paul and Aranha, Dhyan and Pu, Frederick and Hill, Aaron and Hidalgo, Miguel Corredera and Berman, Julian and Tsoukalas, George and Taelman, Lenny , year =. doi:10.48550/arXiv.2603.02668 , url =. 2603.02668 , archivePrefix =

doi:10.48550/arxiv.2603.02668

[23] [23]

doi:10.48550/arXiv.2602.18307 , url =

Xin, Yutong and Chen, Qiaochu and Durrett, Greg and Dillig, Isil , year =. doi:10.48550/arXiv.2602.18307 , url =. 2602.18307 , archivePrefix =

doi:10.48550/arxiv.2602.18307

[24] [24]

doi:10.48550/arXiv.2510.02335 , url =

Yang, Xiao-Wen and Zhang, Zihao and Cao, Jianuo and Zhou, Zhi and Li, Zenan and Guo, Lan-Zhe and Yao, Yuan and Chen, Taolue and Li, Yu-Feng and Ma, Xiaoxing , year =. doi:10.48550/arXiv.2510.02335 , url =. 2510.02335 , archivePrefix =

doi:10.48550/arxiv.2510.02335

[25] [25]

2505.02735 , archivePrefix =

Yu, Zhouliang and Peng, Ruotian and Ding, Keyi and Li, Yizhe and Peng, Zhongyuan and Liu, Minghao and Zhang, Yifan and Zheng, Yuan and Xin, Huajian and Huang, Wenhao and Wen, Yandong and Liu, Weiyang , year =. 2505.02735 , archivePrefix =

Pith/arXiv arXiv

[26] [26]

doi:10.48550/arXiv.2407.11214 , url =

Tsoukalas, George and Lee, Jasper and Jennings, John and Xin, Jimmy and Ding, Michelle and Jennings, Michael and Thakur, Amitayush and Chaudhuri, Swarat , year =. doi:10.48550/arXiv.2407.11214 , url =. 2407.11214 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2407.11214

[27] [27]

Ren, Z. Z. and Shao, Zhihong and Song, Junxiao and Xin, Huajian and Wang, Haocheng and Zhao, Wanjia and Zhang, Liyue and Fu, Zhe and Zhu, Qihao and Yang, Dejian and Wu, Z. F. and Gou, Zhibin and Ma, Shirong and Tang, Hongxuan and Liu, Yuxuan and Gao, Wenjun and Guo, Daya and Ruan, Chong , year =. doi:10.48550/arXiv.2504.21801 , url =. 2504.21801 , archivePrefix =

Pith/arXiv arXiv doi:10.48550/arxiv.2504.21801

[28] [28]

2026 , eprint=

Automatic Textbook Formalization , author=. 2026 , eprint=

2026

[29] [29]

2026 , eprint=

Advancing Mathematics Research with AI-Driven Formal Proof Search , author=. 2026 , eprint=

2026

[30] [30]

2026 , eprint=

A Milestone in Formalization: The Sphere Packing Problem in Dimension 8 , author=. 2026 , eprint=

2026