知识/定理
DeepMind（2024）AlphaProof（与 AlphaGeometry 2）：AI 在国际数学奥赛（IMO 2024）达到金牌水平（4 题满分表现）。
公式
AlphaProof 以 Lean 形式化为自动推理环境，搜索证明；AlphaGeometry 2 专攻几何。
证明思路
强化学习+形式证明搜索：把 IMO 题翻译为 Lean 目标，在证明空间中搜索。
应用/例子
自动定理证明、数学研究辅助、教育。
意义/影响
AI 首次在数学竞赛达人类顶尖；「机器能数学」从传闻到实绩。