Google DeepMind 研究员 Christian Szegedy 判断：全部数学将很快可形式化，证明验证近乎自动化

Google DeepMind 研究员 Christian Szegedy 判断，全部数学将很快可形式化，证明验证近乎自动化。形式化后的证明可像组件一样浏览、重组与搭建，AI 智能体可参与寻找和优化新证明。数学成果或可作为可信黑盒被使用，数学事业则可能高度游戏化，每个未证命题都成为清晰目标。