GPT-6 Astra 在 LeanOpenProblems 中自主找到 Köthe 猜想反例，并提交机器可检验 Lean 证明

Epoch AI 的 LeanOpenProblems evaluation 中，一个预发布 GPT-6 Astra agent 在无人查看或引导 proof search 的条件下，对 Formal Conjectures 中 Köthe 猜想的 Krempa matrix formulation 进行单次自主尝试，找到一个反例并提交 Lean 4 证明。最终 Spec.lean 在独立 pristine container 中由 Comparator 检查与 trusted statement 完全一致，并只允许标准逻辑公理。该原始构造后来由 Adamczewski、Böhmler 与 Marczinzik 做数学检查和推广，并在 9 月 7 日形成更一般的人类论文。