cs.AIOct 24, 2026

Numina Fuse: Interactive Autoformalization in Lean 4

Authors: Justin Asher, Yichuan Cao, Ruichen Qiu, Pietro Pellegrino, Jia Li

Organizations: Project Numina · Academy of Mathematics and Systems Science, University of Chinese Academy of Sciences · University of Naples Federico II

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

Numina Fuse is an agent-native application for formalizing mathematics in Lean 4. Since Lean can compile while not representing its intended informal meaning, and agents now write Lean faster than people can read it, we built Fuse around human supervision of agent work. A user works with an AI orchestrator on a Lean project and supervises it through views of the blueprint, the dependency graph, and the Lean code, while the backend keeps the project's derived state and runs agents for hours without the user present. We describe the development of Fuse throughout 2026, as it moved from a prescribed pipeline of agents paced by human review to an orchestrator that dispatches specialists, provers, and parallel children on its own. We designed for this shift, keeping project state, tooling, and interface design separate from orchestration so that agents could take over more of the work as models improved. We report Fuse's use in a formalization of the three-dimensional Kakeya conjecture and a study of prover models. We close with lessons for the next generation of autoformalization systems. Fuse Desktop, an open-source local version, is available at https://github.com/project-numina/fuse-desktop.

Figures & tables

Figure 1: Fuse’s design phases from March to September 2026, from git history and our internal design records, with the orchestrator’s default model.
Figure 2: Fuse Desktop ( https://github.com/project-numina/fuse-desktop ), the open-source local version, on the Kakeya formalization. Left: the chat with the orchestrator, which narrates its plan, groups its tool calls, and shows provers running as Claude Code subagents ( Prove ml2thick , Prove ml2slab ). Right: the rendered blueprint, with each definition’s label, linked Lean declaration, and formalization status.
Figure 3: Fuse architecture. The orchestrator acts on a workspace through MCP tool servers and a restricted shell, and delegates heavy work to child processes whose events stream back to the backend.
ServerRepresentative tools
blueprintread blueprint and declarations; update entries; set declaration status; refresh metadata
buildbuild project or module; build status, errors, warnings; measure heartbeats
lean-lspgoal state, hover, diagnostics, declaration resolution, Loogle search
lean-exploresemantic search over Mathlib and other indexed packages
sourceslist sources; read text, OCR (lazy, per page), PDF pages as images; search
authoringexplore , draft_blueprint , review_blueprint , formalize , golf , review_proofs
Table 1: MCP tool servers available to the orchestrator. Most are started per session and bound to the session’s clone.
Figure 4: The authoring stages and their order. Shaded stages are writer/reviewer pairs, whose reviewers carry the statement checks. In the pipeline phase, the orchestrator’s instructions and one blocking tool per stage enforced this order; in the final design, each child orchestrator runs these stages in the order its region needs.
Figure 5: Agent layers in a session that delegates. The orchestrator delegates regions of the blueprint to child orchestrators, each in its own Git worktree; up to four run at once (one by default), and their patches are merged into the parent one at a time. Inside each region, specialists and a batch of provers do the work (shown for one region). Host-wide and per-user slot leases bound the total number of child processes.
Figure 6: METR 50% time horizons of frontier models by release date, with 95% confidence intervals [ 39 , 40 ] : the length of task, in skilled-human time, that a model completes half the time. The line is an exponential fit to the models that set a new record when released, doubling every 112 days (METR estimates about 129 days for all models since 2023), dashed where extrapolated. The shaded band is the period in which Fuse was built.
Table 2: Prover models on 52 lemmas, one attempt each, run inside Claude Code with the production prover tools in May–July 2026. Cost per solved lemma includes failed attempts and uses pinned provider prices.
Appendix figures & tables6 assets

Supplementary material from the paper’s appendix.

Appendix

ModelProviderInputOutputCache read
Doubao Seed 2.1 TurboVolcengine Ark0.4172.0830.083
Claude Sonnet 4.6Anthropic3.0015.000.30
Doubao Seed 2.1 ProVolcengine Ark0.8334.1670.167
Claude Opus 4.8Anthropic5.0025.000.50
Kimi K2.6WandB0.954.000.16
DeepSeek V4 FlashAlibaba0.1340.2680.0268
Appendix
Table 3: Prices used for cost, in USD per million tokens. Volcengine Ark prices are converted from RMB at about 7.2 CNY per USD. Cache writes were free on the WandB and Alibaba endpoints.
ModelSolvedTotal $Mean turnsMean wall time (s)
Doubao Seed 2.1 Turbo52/524.1720.0242
Claude Sonnet 4.651/5221.4521.2249
Doubao Seed 2.1 Pro51/528.2417.8175
Claude Opus 4.849/5225.8024.1172
Kimi K2.649/5219.5131.7275
DeepSeek V4 Flash47/521.9125.1383
Appendix
Table 4: Totals per model over the 52 attempts.
Figure 7: The overview in Fuse Desktop, showing the blueprint as rendered text. Each entry carries its number, label, linked Lean declaration, and formalization status.
Figure 8: The blueprint view in Fuse Desktop. The L a T e X source, with its \lean and \leanok markers, sits beside a rendered card for each entry showing its kind and status.
Figure 9: The dependency graph in Fuse Desktop, colored by declaration status (unformalized, formalized, complete), with each node showing its linked Lean declaration.
Figure 10: The Lean view in Fuse Desktop, with the project’s file browser and an infoview tab for the goal state from the language server.
More in this topic

Autoformalization

Autoformalization converts natural-language mathematics, proofs, and specifications into machine-checkable formal languages.

See all 116 papers

Explore similar work

CardsList

  1. LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization

    Jun 3, 2026Yuanhe Zhang, Yuekai Sun, Taiji Suzuki +2Lean Theorem ProvingAutoformalization

    Department of Statistics, University of Warwick, UK · Center for Advanced Intelligence Project, RIKEN, Japan · Department of Statistics, University of Michigan, USA +3

  2. Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning

    Mar 25, 2026Arsen ShebzukhovCycle ConsistencyAutoformalization

    Department of Computer Science, Stanford University

  3. Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance

    Jun 12, 2026Theodore Meek, Siyuan Ge, Di Qiu Xiang +2LLM Agent EvaluationAutoformalization

    Math AI Lab, University of Washington, Seattle, United States · Department of Mathematics, University of Washington, University of Washington, Seattle, United States · Department of Computer Science & Engineering, University of Washington, Seattle, United States +1