Numina Fuse：在 Lean 4 中进行交互式自动形式化

View PDF HTML (experimental)

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 this https URL.

Comments:	16 pages, 10 figures
Subjects:	Artificial Intelligence (cs.AI); Machine Learning (cs.LG); Logic in Computer Science (cs.LO); Software Engineering (cs.SE)
Cite as:	arXiv:2610.33860 [cs.AI]
	(or arXiv:2610.33860v1 [cs.AI] for this version)
	https://doi.org/10.48550/arXiv.2610.33860 arXiv-issued DOI via DataCite (pending registration)

Submission history

From: Justin Asher [view email]
[v1] Sat, 24 Oct 2026 19:05:32 UTC (3,660 KB)