GPT-6 Pro 被公开归因于给出 Nivat 猜想完整证明，GPT-6 Astra Ultra 完成 Lean 形式化

Boon Suan Ho 于 9 月 14 日公开 Nivat conjecture 的 Lean 4 + mathlib formalization，并明确声明完整证明由 GPT-6 Pro 在其 prompts 下生成，论文文本由 AI 起草，Lean formalization 与文档由 GPT-6 Astra Ultra through Codex 生成。仓库将 Challenge.lean 与 Solution.lean 分离，并登记 Palomar；公开验证记录包括 Lean build、Comparator 与 NanoDa 检查。维护者同时明确表示自己不是该领域专家，也没有真正 digest 这份证明。