Google DeepMind 研究员：所有数学将很快可形式化，证明验证近乎自动化

Google DeepMind 研究员 Christian Szegedy 转发判断：所有数学很快将可形式化，证明验证近乎自动化。形式化后证明可像组件一样浏览、重组与搭建，新论文与新想法能被极快检查，智能体可参与寻找甚至发现新证明。数学成果将成为可信黑盒供科学家和普通人使用，数学事业高度游戏化，每个未证命题都是清晰目标。