当AI杀进数学界：Lean 如何成为大模型自进化的练兵场

OpenAI 从千禧年猜想起手、放出七百多份手稿，近期又向 ETH 假设和 P=NP 猜想发起冲击，AI 攻入数学界。核心工具是 Lean 证明系统及其超两百万行形式化内容的 Mathlib，它能把证明转成机器可严格检查的代码。Google 早在 2024 年就用 Lean 搭出 AlphaProof，达到奥数银牌水平。