Lean 能编译，不等于意思对了

在 Lean 4 里写下一个定理，编译器说通过，不代表它写的就是你想说的那件事。这条缝隙，是 10 月 24 日一篇论文整篇在谈的东西。

一、发生了什么

Numina Fuse 是一个面向 Lean 4 数学形式化的 agent 原生应用。作者的判断很直接：Lean 能编译，却不保证形式化语句忠实于原本的非正式含义；同时，agent 写 Lean 的速度已经超过人类阅读的速度。

于是产品做在「人监督 agent」这件事上。使用者和一个 AI 编排器共同推进一个 Lean 项目，通过三样东西监督它：蓝图、依赖图、Lean 代码。后端保存项目的派生状态，能在使用者不在场时连续跑几个小时的 agent。

论文记录了 2026 年全年的演变：从一串按人审节奏推进的固定流水线，变成自己分派专家、证明器和并行子任务的编排器。为了这个转向，他们把项目状态、工具链、界面三者和编排逻辑分开设计，这样模型变强时，agent 能接手更多工作而不用重写产品。

落地用例有两个：三维 Kakeya 猜想的形式化，以及一项关于证明器模型的研究。开源本地版叫 Fuse Desktop，摘要里给了仓库地址。

边界：摘要没有给形式化的规模——多少行、多少引理，也没有人审耗时的量化对比，更没有 agent 写对率这类数字。三个视图具体怎么实现、编排器凭什么决定分派，都要翻正文。作者在摘要里也没有写这套方法的失效场景。

补一点同主题背景。这是背景，不是论文结论：证明助手在数学界已经用于真实项目的协作形式化，社区里长期存在的痛点就是「形式化版本和论文版本对不上」，而这件事只能靠人读，编译帮不上忙。理解这一点，才看得懂他们为什么把人力投在界面上。

二、跟你有什么关系

做数学形式化的课题组：你缺的可能不是更强的证明器，是让人跟得上的审阅界面。蓝图加依赖图这两个视图，比再训一个模型便宜。

做 AI 编程工具的：这条经验可以整体搬走。当生成速度超过阅读速度，产品价值就从「写出来」转到「让人敢合并」。

考虑押注数学 AI 的团队：三维 Kakeya 这个案例说明工具已经能承接真实的前沿问题，但承接方式是「人盯 agent」，不是「agent 交作业」。

三、怎么用

1. 先写蓝图，再让 agent 写代码。没有依赖图，你判断不了它新加的这个引理是不是在绕路。
2. 把交付单元切成一个引理。一次让它交三百行，人审必然退化成抽查。
3. 拿开源本地版先跑小项目，只记一个数：你读它写的代码，比它写代码慢多少倍。这个倍数决定你能开多大的项目。

四、三个别信的说法

「Lean 编译通过就说明形式化对了。」 论文开篇就在反驳这句。编译只保证语法和类型合法，语义对不对得上原题，得人来判。

「agent 写得快，项目就推得快。」 瓶颈已经移到审阅侧。生成速度涨十倍，人审速度不变，整体只会更堵。

「自动形式化迟早取代人。」 这篇的整个设计前提相反：正是因为 agent 写得太快，人的监督角色才需要被产品化。

五、一句话结论

形式化的瓶颈已经从「写不出来」变成「读不过来」，工具该围着人的注意力设计。

信息来源

• arXiv：Numina Fuse，Lean 4 里的交互式自动形式化（2026-10-24）

功能与价格以官方公告为准。本文写于 2026 年 10 月 27 日。