OpenAI人工智能数学当 AI 开始探索数学未知，我们该兴奋什么？

OpenAI 10 月 6 日公布了一批由内部前沿模型产出的数学成果，并公开了多项证明的 Lean 形式化版本，让计算机可以检查其逻辑。

我最关注的是：这些成果能否经得起检验，又能帮助人类提出哪些新问题？

生成证明、验证证明、理解证明，是不同的工作。机器检查能帮助确认形式化推导，但问题是否被准确表达、成果有何价值、前人贡献是否得到尊重，同样需要认真对待。

如果 AI 能加速探索，人类就更有机会把时间投入到理解与创造中。这是我对这次进展最大的期待。

突破值得期待，证明需要检验。

你认为，AI 会怎样改变数学家的工作？