OpenAI 系统参与发现 112 顶点 Petersen coloring counterexample，并公开 SAT / DRAT 可复核证书

Bryce Putman 给出一个 112 顶点 simple bridgeless cubic graph，没有 Petersen coloring，也没有 normal 5-edge-coloring；论文公开图的 SHA-256、SAT encodings、CaDiCaL UNSAT 结果、DRAT proofs 与重建程序。论文的 computational provenance section 披露 OpenAI language-model systems 广泛参与 discovery、computational search、verification 与 preparation。次日 Jorik Jooken 又给出短的人类可检查证明。