Numina Fuse：Lean 4 中的交互式自动形式化
Numina Fuse: Interactive Autoformalization in Lean 4
AI 导读
Numina Fuse 是一个面向 Lean 4 数学形式化的智能体原生应用，用户通过蓝图、依赖图和 Lean 代码视图监督 AI orchestrator 的工作，后端可在用户不在场时运行智能体数小时。2026 年间它从人工审核驱动流水线演进为自主调度专家、证明器和并行子任务的编排器，并已用于三维 Kakeya 猜想的形式化。开源本地版本 Fuse Desktop 已可用。
正文 · 原文
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)
来源：arXiv cs.AI · arxiv.org