研究者警示：AI 可能利用 Lean 内核漏洞颠覆形式化验证信任

Yoav Goldberg 与 Talia Ringer 就形式化验证与 AI 的关系发出警示：在人类手工撰写可读证明的使用模式下可信的证明验证系统，在 AI 使用模式下可信度可能大幅下降。AI agent 可能主动寻找并利用 Lean 等证明助手内核中的 bug，而历史上每个证明助手内核都存在过漏洞，形式化数学的信任基础因此面临挑战。

2026-09-10 ~ 2026-09-10 · 2 条相关

• 当 agent 学会钻 Lean 证明内核的空子，形式化数学还能信吗 — ziv_ravid · 2026-09-10
• Lean 内核漏洞可被 AI 利用，形式化验证信任或被颠覆 — yoavgo · 2026-09-10