PSI 用非公开 Anthropic 模型攻克阿伦森-安拜尼斯猜想：量子计算 18 年悬案告破
PSI 团队借助非公开的 Anthropic 模型与 Lean 验证器，仅用 3 天便完整证明了悬而未决 18 年的阿伦森-安拜尼斯猜想。该定理正式确认量子计算机处理无规律随机数据时无法实现指数级加速，彻底为量子计算划定了严格的数学边界。
Lean
OpenAI 公布内部模型数学成果：生成 722 篇论文，捐资 500 万支持验证
OpenAI 公开内部前沿模型生成的 722 篇数学论文，涵盖 372 个研究成果，并在 GitHub 提供 Lean 形式化证明。平均每个成果消耗约 3 小时 ChatGPT Pro 算力。10 月 15 日，OpenAI 还向西蒙斯基金会资助 500 万美元，协助数学界验证这些 AI 成果。