Numina Fuse is an agent‑native application designed to assist users in formalizing mathematics with Lean 4. While Lean can compile code, it does not always capture the intended informal meaning, and modern AI agents now write Lean code faster than humans can read it. Fuse therefore places human supervision over agent work: a user collaborates with an AI orchestrator through three views—blueprint, dependency graph, and raw Lean code—while the backend keeps the project's derived state and lets agents run for hours without the user present.
During 2026 the system evolved from a prescribed pipeline that required human review to an orchestrator capable of dispatching specialist agents, provers, and parallel child processes on its own. The architecture deliberately separates project state, tooling, and interface design from the orchestration layer, allowing agents to take over more tasks as model performance improves without redesigning the front end.
Fuse has been applied to a formalization of the three‑dimensional Kakeya conjecture and to a study of various prover models. An open‑source desktop version, Fuse Desktop, is available at https://github.com/project-numina/fuse-desktop.
Review