AI agents 发现 Jackson Hamilton decomposition conjecture 的 12 顶点反例，并由 Lean kernel 检查

Lech Mazur 公开一个 12-vertex regular bipartite tournament，满足每个顶点 indegree=outdegree=3，却不存在 Hamilton decomposition，从而反驳 Jackson 的 unrestricted conjecture。ProofAtlas 将其记录为通过 AI agents 发展出的 checked counterexample；Lean build 通过、无 unfinished proof steps，并将 publication status 标为 accepted formal theorem。