GPT-5 prover/verifier 协议用 Lean 校验自然语言数学：解决 2025 IMO 5/6，并关闭 66 个数论猜想约三分之一

Le Duc 与 Liberti 采用多个 GPT-5 instances 扮演 prover / verifier 的协作协议，最终证明再由 Lean proof assistant 验证，且由人类检查 Lean premises / conclusion 与原始命题是否一致。论文报告该方法解决 2025 IMO 6 题中的 5 题，并关闭 Cohen 提出的 66 个 number-theory conjectures 中约三分之一。