“通过 Lean 检查”要说明被谁检查
AI 产出的证明多到没人逐行读时，检查器就是唯一的信任点，而按 de Moura 的说法，AI 也最会找它的漏洞。所以一项“在 Lean 中证明”的结果，要看用了几个独立内核、是否过了 comparator 一类的复查。这是我们从他的说法得出的读法。
AI FOR SCIENCE · 访谈
AI 写证明之后，Lean 的检查本身成了被攻击的对象
- 公司
- Lean FRO
核心信号
de Moura 说，一个号称推翻 Collatz 猜想的假证明同时骗过了 Lean 的官方内核和外部内核 nanoda，各钻一个不同的漏洞，他们相信是 AI 造的。他的结论是：检查器要多个、要公开、要逐步被证明正确，而证明只担保人写下的那条命题。
这次新增
Lean 的负责人讲出这次漏洞的经过和补救（官方内核已修，comparator 改成总用最新版 nanoda），并给出数字：Mathlib 现有 240 万行，自 2025 年增长 44%、编译时间反降 10%；要能形式化任意研究论文，社区估计要 1 亿行。
当前边界
官方内核还没有被证明正确：Mario Carneiro 的 Lean4Lean 只证明了一部分，没覆盖这次被利用的地方；生成可执行程序时编译器也在信任范围内，尚未验证。
访谈里说了什么
绿色对勾也会说谎
按 de Moura 的经过：nanoda 先被报了一个漏洞并当即修好；几天后有人提交一份 Collatz 的 Lean“反证”，官方内核接受，修复前的 nanoda 也接受。证明里塞了一堆与问题无关的项来制造哈希碰撞，只为骗过 nanoda。提交者说是巧合，他们则不能排除模型自己读了 nanoda 的修复、再造出这个漏洞利用。
“We strongly believe it was built by AI.”Leonardo de Moura
办法是多个内核、公开、证明正确，不是藏起来
他要更多由不同人、用不同语言写的独立内核，最终要一个被证明正确的内核（Lean4Lean），再往下是验证过的编译器。主持人提议像 ARC-AGI 那样留一个不公开的内核，他拒绝：信任要靠透明，不能靠保密。
证明只担保人写下的规格
Kim Morrison 用 Claude 智能体把 zlib 从 C 翻成 Lean，通过 C 版的测试，并证明任意压缩级别、任意数据压缩再解压都还原原文。de Moura 说这年初他还以为做不到；但证明的只是这条性质，选什么性质仍是人的责任。
模型擅长拼已有的招，不擅长发明新招
他说现在的模型在“nut-sniping”上已胜过人：命题给定、不需要新理论、只要把现成的部件拼起来；让它们想一个新技巧，就“惨败”。它们的记忆像给下一次醒来留的面包屑，权重并没有在学。
瓶颈在库，不在单个证明
形式化一篇论文是否可行，取决于背景材料在 Mathlib 里有没有。Mathlib 现在 240 万行，社区估计要到 1 亿行才能形式化任意研究级论文。Mathlib Initiative 的 Formal Frontiers 想让人加 AI 补齐缺口，用费马大定理这类好陈述、难证明的定理当里程碑。
改变了什么
- 此前的公开记录→
记录里的 Lean 条目把通过检查当作终点：Claude 完成费马大定理的形式化（2026-09-04）记为“计算机可检查”。记录里没有一条说检查器本身会出错。
这次访谈新增Lean 的负责人说，一个假证明刚刚骗过了官方内核和一个外部内核，他们相信是 AI 造的，而且这种事“还会一再发生”。
- 此前的公开记录→
时间线在 2026-09-29 之前没有一条 Lean 本身或 Lean FRO 的条目。
这次访谈新增Lean FRO 约 20 人；官方内核已修；comparator 在沙箱里导出并复查证明，改为总用最新版 nanoda；内核悬赏、简化内核还只是在讨论的想法。
- 此前的公开记录→
记录里的数学条目讲的是单个结果，没有 Mathlib 的规模或增长数字。
这次访谈新增Mathlib 3 停在 110 万行，Mathlib 4 现在 240 万行，自 2025 年增长 44%、编译时间降了 10%；AI 写数学之后，他说库的增长会快过他们优化性能的速度。
为什么重要
人的审查要挪到命题和定义上
zlib 那个例子里，机器证明了人选的性质，没有证明人没选的。他把人的位置放在规格、定义、Mathlib 的路线图和关键证明的写法上。投入审查的人力，应当花在形式化的命题是否真是要证的那个问题。
能形式化多少，取决于库
按他的说法，缺了背景材料，形式化一篇论文要从头搭基础设施；240 万行与估计的 1 亿行之间，是 AI 加速最可能见效、也最需要人把关结构的地方。
主张与边界
主张谁的口径目前状态
一份 Collatz 的 Lean“反证”同时被官方内核和修复前的 nanoda 接受，分别利用两个不同的漏洞；他们“强烈相信”是 AI 造的，提交者说两个漏洞重合是巧合。
公司自述
de Moura 的说法；文字稿引用的 Lean issue 与修复本页没有打开。是否 AI 所造是推断，不是确认。
官方内核的漏洞已由他修复；comparator 若当时用的是最新版 nanoda，就会拒绝这份证明，现在已改成总下载最新版。
当前系统
de Moura 的描述，没有读到 Lean FRO 的书面说明。
Claude 智能体把 zlib 从 C 翻成 Lean，通过 C 版测试，证明了压缩再解压还原原文；优化后的版本“胜过我们的 Rust 实现”。
公司自述
项目由 Lean FRO 的 Kim Morrison 主导，由 de Moura 讲述；“我们的 Rust 实现”指哪一个、快多少，访谈没有说。
Mathlib 3 停在 110 万行，Mathlib 4 现有 240 万行；自 2025 年增长 44%，编译时间降 10%。
公司自述
de Moura 的数字；没有读到原始统计。
要能形式化任意研究级论文，Mathlib 需要约 1 亿行。
行业背景
他转述的社区估计，没说出处。
OpenAI 推翻单位距离猜想的结果，由 Boris Alexeev 提交了一份 120 万行的 Lean 证明。
行业背景
他引来说明证明会大到没人读；本页没有读那份证明。
模型在组合已有技巧上胜过人，在发明新技巧上失败；GPT 5.6 和 Claude Fable 胜过用蒙特卡洛树搜索的系统，但哪种更便宜还没定论。
受访者判断
他的判断，成本一点转述同事在会上的实验，没给数字。
内核还没被证明正确；生成可执行程序时，编译器也在信任范围内，尚未验证。
尚未闭环
de Moura 自己明确说明，并列为接下来的工作。
接下来看什么
Lean FRO 有没有书面公开这次漏洞的两处原因，以及此后有没有 AI 造的漏洞利用穿过 comparator。
会表现为 Lean FRO 自己的事后说明，或一个新的内核 soundness issue。Lean4Lean 能不能完成，成为一个被完整证明正确的内核，覆盖这次被利用的部分。
会表现为 Mario Carneiro 发布的完整正确性证明。自称“在 Lean 中证明”的 AI 数学结果，会不会写明用了哪些内核、是否过了 comparator。
会表现为 论文或代码库里自己的检查记录。部分回答 AlphaProof Nexus 的《科学》论文（10 月 8 日）写明了检查：每个证明用 SafeVerify 对照定理命题核验、防注入公理之类的漏洞，命题由团队专家逐一核对；但没说用的是哪个内核、有没有第二个内核复查。北大的庞加莱形式化（10 月 6 日）写了独立内核复查；OpenAI 的 722 篇手稿（10 月 6 日）只说多数而非全部已形式化。Formal Frontiers 会不会公布里程碑定理，以及有没有一个 AI 搭起来的库证明到其中一个。
会表现为 Mathlib Initiative 公布的清单和一份能通过检查的证明。lean-zip 胜过 Rust 的说法，会不会附上基准测试公开。
会表现为 代码库里写明对比对象、数据和硬件的测试结果。
采访之后
后来出现的、检验或限制这次说法的证据，以及日期已过的目标。
北大团队用编码智能体完成庞加莱猜想的 Lean 形式化，论文说结果通过完整构建、与只用 Mathlib 写成的目标命题核对，并用一个独立内核复查：正是 de Moura 说的多内核和命题复查。命题是否准确表达 Perelman 的证明，论文仍交给人审，与他“证明只担保规格”的说法一致。时间线条目 →
OpenAI 一次公开 722 篇数学手稿，称多数而非全部已形式化，Altman 说四项头条里三项有 Lean 证明。这正是 de Moura 说的规模：没人会逐行读；而 Lean 证明只检查每一步，不检查形式化表述是不是那个开放问题。时间线条目 →
AlphaProof Nexus 的同行评审版发表在《科学》。论文写明每个证明都用 SafeVerify 对照定理命题核验，防的正是注入公理一类的环境漏洞；团队专家逐一核对 9 个 Lean 命题是否就是 Erdős 的原题，智能体的证明还暴露出两道题里“密度”的含义不清，改正命题后仍然解出。这印证了 de Moura 说的：证明只担保写下的命题，命题要人来审。论文没说是否有第二个内核复查。时间线条目 →
读于 2026.10.08 节目方发布的带说话人标注的完整文字稿，通读，并对照节目简介。文字稿为 Collatz 事件引了 Lean 和 nanoda 的 issue 与修复，本页没有打开这些页面，所以那段经过是 de Moura 的说法。 打开原访谈 ↗播客节目页 ↗节目方的完整文字稿（ReScript） ↗