Numina Fuse：Lean 4 中的交互式自动形式化

Numina Fuse 是一款用于在 Lean 4 中形式化数学的智能体原生应用。由于 Lean 代码即便能够编译通过，也可能未能表达其预期的非形式化含义，而如今智能体编写 Lean 代码的速度已超过人类阅读的速度，因此我们围绕人类对智能体工作的监督构建了 Fuse。用户与 AI 编排器协作处理 Lean 项目，并通过蓝图、依赖图和 Lean 代码视图进行监督；后端则维护项目的派生状态，并在用户不在场的情况下持续运行智能体数小时。我们介绍了 Fuse 在整个 2026 年的发展历程：它从一套由人工审核控制推进节奏的预设智能体流水线，演变为能够自主调度专家智能体、证明器和并行子智能体的编排器。我们在设计中为这一转变做好了准备，将项目状态、工具和界面设计与编排机制分离，以便随着模型能力的提升，让智能体接手更多工作。我们报告了 Fuse 在三维 Kakeya 猜想形式化及一项证明器模型研究中的应用。最后，我们总结了面向下一代自动形式化系统的经验。Fuse Desktop 是一个开源的本地版本，可在 https://github.com/project-numina/fuse-desktop 获取。