姚班校友主导，Claude 攻克费马大定理首个完整形式化证明

3 小时前

清华姚班校友Tianyi Peng主导，Anthropic的Claude仅耗时11天，便完成了费马大定理首个端到端、可由计算机完整检查的形式化证明。该证明产生了约1300万行Lean代码，超过3万个中间定理，代码规模是Lean核心数学库Mathlib的5倍多。此次工作是将人类可读的证明转化为计算机可逐行验证的形式化证明，过程中多Agent协作曾出现混乱，后通过Prove2Me平台得以理顺，人类仅提供了少量高层提示。此外，OpenAI正逐步向ChatGPT付费用户开放GPT-6 Astra，该模型在长链路Agent任务等多项能力上有所强化。