形式化验证 (Lean)
使用Lean等工具，将数学证明转化为计算机可验证的代码，确保其绝对严谨。在AI数学发现的语境下，形式化验证解决了AI证明可能存在的"幻觉"或"隐藏bug"问题，是AI成果被学界接受的关键保障。
在Erdős Problem #1196事件中的作用
Math Inc.的"Gauss"团队只用5小时，就用Lean形式化语言把ChatGPT 5.4 Pro的证明写成7000多行代码，后优化到4000行。Lean是数学界公认的"铁证"，一旦通过，就等于在形式逻辑层面盖了章，没人能再挑刺。erdosproblems.com官网将#1196标记为"PROVED（LEAN）"。
对AI与真理关系的影响
形式化验证为[[大模型不是真理机器-而是论证机器]]这一概念提供了一个重要的"例外与延伸"：在形式化验证框架下，AI的"论证"可以转化为"真理"。这提示我们需要更新对"大模型与真理关系"的理解，尤其是在有严格验证框架的领域。
相关链接
- [[ai-solves-math-problems]]
- [[math-inc-gauss]]
- [[erdos-problem-1196]]
- [[大模型不是真理机器-而是论证机器]]