Numina Fuse 是面向代理的应用，旨在帮助用户在 Lean 4 中完成数学形式化。Lean 能够编译代码，却不一定捕捉其背后的非形式含义；而如今的 AI 代理写 Lean 代码的速度已经超过人类阅读的速度。为此，Fuse 将人类监督置于代理工作之上，用户通过蓝图视图、依赖图以及 Lean 源码三种界面与 AI orchestrator 交互，后端持续维护项目的派生状态，并让代理在用户离线时持续运行数小时。
在 2026 年的迭代过程中，Fuse 从最初需要人工审查的固定流水线，演进为能够自行调度专家代理、证明器以及并行子任务的 orchestrator。系统设计上将项目状态、工具链和界面设计与调度逻辑解耦，使得随着模型能力提升，代理能够接管更多工作而无需重新构建前端。
Fuse 已在三维 Kakeya 猜想的形式化以及一系列证明模型的实验中得到验证。项目的开源桌面版 Fuse Desktop 可在 https://github.com/project-numina/fuse-desktop 获取。
点评