Numina Fuse: Interactive Autoformalization in Lean 4

1 Introduction

• Fuse was designed for human experts to review formalization faithfulness and quality, with reviewer agents and statement review, dependency-graph support for reuse, and interruptible agent actions to address drift.The user can review the blueprint, formalization, and agent actions in real time.Source: §1 · p. 1
• The interface presents the blueprint, dependency graph, Lean code, goals, errors, and live agent actions; backend state and sessions persist after the browser closes.Users can redirect agents or edit blueprint and Lean code directly; results are reviewed as pull requests.Source: §1 · p. 1
• Fuse evolved from a single agent to a prescribed writer-reviewer-prover pipeline, then to an orchestrator dispatching long-lived specialists, prover batches, and parallel delegated orchestrators.The orchestrator-led design is shown in Figure 1.Source: §1 · pp. 1–2, Figure 1 · p. 2
• Fuse separates project state, Lean tooling, and interface design from orchestration so agents can take on more work as models improve.This design reflects the authors’ expectation that general methods scaled with better models can overtake hand-built structure.Source: §1 · p. 2
• During the three-dimensional Kakeya formalization, a researcher using Claude Opus 5 and Claude Fable 5.1 outside Fuse formalized the remainder of the proof in the final two weeks.The crossover came when swarms of unmonitored agents became more effective than user-guided agents.Source: §1 · p. 2
• The paper describes the hosted system; Fuse Desktop shares its interface and agent roles but omits hosted prover routing, delegation, sandboxing, and metering.Desktop is a single-user local version using the user’s Claude Code or Codex account.Source: §1 · p. 2
• The paper contributes a deployed formalization environment, a six-month account of design changes and failures, and Kakeya deployment experience with a prover selection and cost study.The contributions cover Sections 2–6 and 8.Source: §1 · p. 2

2 Using Fuse

• A Fuse project is a GitHub repository with one or more Lean packages; a workspace attaches a blueprint to a repository branch and organizes its papers, graph, blueprint, and Lean editor.Blueprint declarations link informal statements to Lean declarations and show whether they are not started, formalized, or proved.Source: §2 · p. 2
• Users ask the orchestrator for an outcome, steer it at any point, and receive streamed tool calls, edits, and build errors while sessions continue in the background.Sessions survive browser closure and notify the user when attention is needed.Source: §2 · p. 2
• People caught three Kakeya statement errors after the fact, and work reaches the main branch only through a pull request a person merges.The errors included an unsatisfiable hypothesis, a Lean statement stronger than its blueprint entry, and a false quotient statement.Source: §2 · p. 3

3.1 What lasts and what changes

• Fuse keeps repository work in an ordinary Lean and leanblueprint project, stores derived state in the backend, and changes orchestration prompts, roles, and dispatch rules as models change.The design separates project state, tooling, and interface from orchestration.Source: §3.1 · p. 3

3.2 Components

• The React views read from a FastAPI backend that streams agent and workspace events; each session’s orchestrator acts through MCP servers and child processes on a repository clone.The backend builds each clone with a Lean service and stores durable state in PostgreSQL, leaving the browser as a view.Source: §3.2 · p. 3, Figure 3 · p. 4

3.3 Project state

• A workspace attaches a blueprint to a managed repository branch, while its parser extracts declaration labels, linked Lean names, dependencies, and proof blocks.Parser-owned fields are recomputed on refresh, while agent-owned assessments and notes are written by agents.Source: §3.3 · p. 4
• Fuse tracks recorded blueprint status, Lean-checked compilation without errors or sorry, and faithfulness review by reviewer agents or people.These checks are deliberately light: axiom checks and statement comparisons are not run after every turn; the Kakeya release was checked separately by rebuilding the library and checking the main theorem’s exact axioms.Source: §3.3 · pp. 4–5

4 Agents

• An OS jail with namespaces and resource limits surrounds each agent process, supplementing an allowlisted shell and clone-confined paths because builds can run arbitrary code during elaboration.The permission gate also refuses writes to Git internals and CI workflows; only the backend commits and pushes.Source: §4 · p. 5
• Specialists cover blueprint writing and review, formalization and review, API exploration, proof shortening, proof-style review, and proving.The explorer searches Mathlib and indexed packages so writers and provers can reuse existing results.Source: §4 · p. 5
• Reviewers return declaration-level verdicts and communicate findings to writers; blueprint reviewers check counterexamples and unsatisfiable hypotheses, while formalizer reviewers compare Lean statements with blueprint entries.Reviewer responsibilities increased after statement errors were found in the Kakeya formalization.Source: §4 · p. 5
• Proof search uses batches of up to eight provers, one per declaration, each working in a scratch copy of its file with an inexpensive model.The agents run as separate Claude Code processes.Source: §4 · p. 5
• Fuse’s orchestrator now dispatches autonomous sessions, delegates regions and builds in the background, and decides when to delegate and collect results, while remaining barred from writing proofs itself.The earlier pipeline used a fixed stage order and effort levels; the final design dropped effort levels but retained the proof-writing restriction through tool permissions.Source: §4 · p. 5
• Each delegated region runs in a detached worktree, so partial or failed child work does not touch the parent; up to four children can run at once, but patches merge one at a time.Delegation is one level deep, and children cannot delegate further.Source: §4 · pp. 5–6
• As agent time horizons rose, short-task mechanisms were removed first: effort-level retries gave way to autonomous sessions, and enforced writer/reviewer loops gave way to standing specialists.Apart from the prover study and golfer heartbeat reductions, these design changes were not measured.Source: §4 · p. 6

5 Infrastructure and operations

• Each workspace clone has one Lean language server shared by agents and the browser’s Lean view, while child orchestrators check worktrees with separate Lean runs.Build errors are stored by file hash, and a known error in a changed Lean file blocks a commit.Source: §5 · p. 6
• The backend commits and pushes workspace changes, rebases and revalidates rejected pushes, and uses a bounded merger agent for branch merges; people and agents can edit the blueprint concurrently through Yjs.Commits can occur after agent turns, on manual commit or save, or when the last editor disconnects.Source: §5 · p. 6
• Fuse meters every model call, including OCR and title generation, and stops a user’s sessions when daily or weekly caps are reached.Users linking their own Claude subscription have its Claude-agent spend excluded from Fuse’s caps.Source: §5 · p. 6
• Long sessions stay routed to the release that owns them during deploys; schema-changing deploys pause sessions, record resumption instructions, and restart them on the new release.New sessions go to the current release.Source: §5 · p. 6
• Figure 4 marks writer/reviewer pairs with shading and contrasts the pipeline’s enforced stage order with child orchestrators’ region-specific ordering.The pipeline enforced order through orchestrator instructions and one blocking tool per stage.Source: Figure 4 · p. 6
• Figure 5 shows delegated blueprint regions in separate Git worktrees, with up to four child orchestrators running at once and patches merged into the parent one at a time.Each region’s specialists and prover batch do the work, while host-wide and per-user slot leases bound child processes.Source: Figure 5 · p. 7

6.1 Prover selection and cost study

• The prover study tested seven models on 52 lemmas from four developments, with one attempt per lemma and kernel-replayed proofs counted as solved.Each attempt was limited to 80 turns and 30 minutes; cost per solved lemma includes failed attempts.Source: §6.1 · p. 7
• All seven prover models solved 45–52 of 52 lemmas, while cost varied by more than an order of magnitude, motivating inexpensive proof search at similar accuracy.Proof search therefore goes to inexpensive models while a frontier model orchestrates.Source: §6.1 · pp. 7–8

6.2 Kakeya in dimension three

• The released repository discharges StickyFrostmanHypothesis through an independent formalization, yielding Unconditional.KakeyaDimensionThree.The main theorem’s type takes the hypothesis as an explicit input.Source: §6.2 · p. 8
• Review findings prompted stronger reviewer checks and an explorer agent; the golfer reduced one central file’s elaboration work by about 61%.The file’s count fell from about 220M to 85M heartbeats.Source: §6.2 · p. 8
• The final assembly used Claude Fable 5.1 outside Fuse to find and repair a vacuously provable Proposition 6.6 statement.The repaired statement was proved and certified to have satisfiable hypotheses.Source: §6.2 · p. 8
• The final assembly added about 592k Lean lines in 12 days, at two to five times the daily rate of one-session-at-a-time Fuse work.Excluding roughly 35% copied from other branches leaves at most 288k new lines, or 25k per day.Source: §6.2 · pp. 8–9

Blueprint-driven formalization

• Blueprint-driven projects develop informal blueprints alongside formal proofs, while Fuse assigns drafting, formalization, and proof search to agents but leaves statements to people [5] [6].LeanArchitect instead generates blueprints from annotated Lean [68].Source: §7 · p. 9

Agentic autoformalization systems

• Related agentic systems combine blueprints, specialized agents, and review; Fuse distinguishes itself with an ordinary leanblueprint document, explicit golfing and style stages, and frontier coordination separated from inexpensive provers [65] [34] [16] [63] [7].The surveyed systems range from human-supervised workflows to large-scale autonomous agents.Source: §7 · p. 9

Provers

• Prover work ranges from whole-proof and step-level models to agentic frameworks, while Fuse treats models as interchangeable workers rather than competitors [60] [47] [56] [32] [33] [13] [61] [58] [12] [26] [42] [67] [55] [48].The passage also describes PutnamBench as saturated and miniF2F as effectively solved [54] [66] [16] [55].Source: §7 · p. 9

Statement faithfulness

• Prior audits report substantial statement-faithfulness gaps, supporting Fuse’s blueprint reviewer’s practice of checking for counterexamples first [64] [49] [18] [30] [17].The passage notes that type-checking alone does not rule out translation errors [30].Source: §7 · p. 9

Agent harnesses and multi-agent systems

• Harness research describes hand-built scaffolding as potentially stale or task-dependent, alongside emerging orchestrator–worker systems and models trained for parallel subagent use [59] [57] [24] [44] [29].Fuse starts each child through its own MCP tools so it inherits Fuse’s permission checks.Source: §7 · pp. 9–10

Blueprints are now a bottleneck

• A separately maintained blueprint can add work, become outdated, and constrain agent decomposition, so the authors expect a graph of Lean statements to support more adaptive planning and reuse.Agents could choose what to attempt next from the graph as the decomposition changes, without maintaining a separate document.Source: §8 · p. 10

People should set standards, not review every step

• The authors recommend reducing routine intermediate-lemma checkpoints while retaining human review of definitions, main theorem statements, and release acceptance.They argue that people should set standards for what to formalize and what counts as a good formalization.Source: §8 · p. 10

Architecture and search are more important

• As proof writing improves, library architecture and search matter more: people and agents need to find reusable results by informal description or type and recognize equivalent formulations.The passage contrasts proof- and lemma-level tools with questions about definitions, development fit, and APIs for later projects.Source: §8 · p. 10

Progress now depends on infrastructure and institutions

• The authors call for a coordinated, sustained initiative and shared destination for formalized mathematics, citing the proposed Mathematics Autoformalization Project.They identify access to papers and compute, plus building, verifying, and maintaining mathematics across toolchain changes, as possible constraints.Source: §8 · p. 10

Conclusion

• Fuse brought human statement review, agent proof search, persistent project state, and Lean verification together in one environment.Source: §9 · p. 10
• Over 2026, Fuse moved from a prescribed agent pipeline toward an orchestrator that chooses its own dispatch.Source: §9 · p. 10
• Fuse supported the Kakeya formalization and a prover study; the authors identify project state, Lean tooling, and verification as the parts that lasted beyond a particular model.Source: §9 · p. 10

• 52 lemmas from four developments were tested in Lean v4.30.0-rc2 with Mathlib 7ea6142b3f, using fresh directories and a proved Machinery module for each target.Each Challenge module stated its target with sorry; the agent filled a copy.Source: A Prover study data · p. 14
• Solutions counted only when leanprover/comparator accepted them with axioms limited to propext, Quot.sound, and Classical.choice.Models used the production prover prompt and specified tools, with up to 80 turns and 30 minutes per attempt.Source: A Prover study data · p. 14
• Table 3 lists costs in USD per million tokens, with Volcengine Ark prices converted from RMB at about 7.2 CNY per USD.Cache writes were free on the WandB and Alibaba endpoints.Source: Table 3 · p. 14
• Table 4 reports totals per model over the 52 attempts.Source: Table 4 · p. 14

• The gallery shows Fuse Desktop, the open-source local version, on the Kakeya formalization, with orchestrator chat open on the left in each view.Source: B Interface gallery · p. 15
• The blueprint overview renders entries with their number, label, linked Lean declaration, and formalization status.Source: Figure 7 · p. 15
• The blueprint view pairs LATEX source containing \lean and \leanok markers with rendered cards showing each entry's kind and status.Source: Figure 8 · p. 15
• The dependency graph colors declarations by status—unformalized, formalized, or complete—and links each node to its Lean declaration.Source: Figure 9 · p. 16
• The Lean view combines the project's file browser with an infoview tab showing the goal state from the language server.Source: Figure 10 · p. 16