Lean 是一种交互式定理证明器，近年来与人工智能的结合成为数学研究的热点。近期，一系列工作展示了AI在Lean中形式化证明的强大能力，但也引发了对方法可靠性的争议。
- 主要进展
- Google DeepMind AlphaProof Nexus 以数百美元解决56年未解数学难题：AlphaProof系统将AI推理与Lean形式验证结合，低成本地攻克了多个长期悬而未决的数学问题，验证了AI辅助数学证明的经济可行性。
- Claude Code 在 Lean 4 程序验证中达 98.1% 成功率：Claude Code在Lean 4环境中的程序验证测试取得极高通过率，表明大型语言模型在形式化证明任务中具备实用潜力。
- AI 驱动形式化证明搜索攻克 9 个 Erdős 开放问题：另一团队利用神经符号方法搜索Lean中的证明，解决了9个未解决的Erdős问题，证明AI可发现新颖推理路径。
- Gary Marcus 质疑新数学成果：神经符号还是纯LLM？：Gary Marcus对部分成果的方法提出质疑，认为应区分真正的神经符号创新与纯LLM的统计生成，引发对AI数学严谨性的讨论。
- CAM-Bench：面向计算与应用数学的Lean 4定理证明基准：学术界发布了专门针对计算与应用数学的Lean 4基准，为评估AI形式化证明能力提供了标准化测试集。
当前焦点与未来观察
当前争议集中于AI证明的“方法本质”——是真正的符号推理还是统计模式匹配？未来需更透明的评估基准和跨方法比较。此外，Lean与AI的结合正从纯数学向程序验证和科学计算扩展，但其可靠性和可解释性仍是关键挑战。