OpenAI声称利用内部版Astra模型和GPT-5.6的token价格，以每个问题不到2000美元的成本解决了十个长期未攻克的数学难题。结果包含Lean 4形式化验证和论文，但使用的提示词尚未公开。此举紧随Anthropic用Claude发现密码学弱点之后，再次引发关于AI在数学研究中作用的讨论。
背景
OpenAI和Anthropic正越来越多地使用大语言模型解决形式化数学问题，结果通过Lean 4等证明助手验证。这一趋势在数学界引发了兴奋与担忧，关于AI在研究中的角色日益增强。
- 来源
- Simon Willison
- 发布时间
- 2026年8月2日 04:34
- 评分
- 7.0 / 10