What was already known
Klostermeyer and Mynhardt’s equality conjecture held in several restricted graph classes. The underlying Berlekamp–van Lint–Seidel graph was already known.
AI involvement
The human paper says GPT-6 Astra found the counterexample graph in an experiment run by Tom Adamczewski. The repository credits the model with the Lean proof; Adamczewski set up the experiment, while William F. Klostermeyer supplied the paper's mathematics and stronger clique-cover argument.
The model found the retained counterexample graph and authored its Lean proof inside a human-set experiment; the human paper's mathematics and strengthening belong to Klostermeyer.
Importance
Gives an explicit counterexample to the unrestricted equality conjecture.
Limitations
Klostermeyer’s separate human paper strengthens the clique-cover lower bound to at least 5. The AI-origin claim is the graph and its stated 3<θ witness.
Technical verification
At the cited repository revision, the source reports a completed Lean proof without admitted declarations of gamma=gamma-infinity=3<theta for the explicit graph. Finite common-neighbor facts use kernel evaluation and the remaining argument is symbolic. The paper's independent exhaustive program supports the same graph but its separate proof is not treated as a human check of the Lean argument.
Formal checking
Lean theorem with kernel-checked finite common-neighbor table and symbolic guard-strategy and coloring arguments
- Checker
- Lean 4 proof development released by Tom Adamczewski
- Scope
- The explicit 243-vertex complement has gamma=gamma-infinity=3<theta in the one-guard-moves model
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Klostermeyer's paper and the repository explain the common-neighbor construction, why three guards can defend every attack, and why a three-clique cover fails for the same graph.
Correction and publication history
Gives an explicit counterexample to the unrestricted equality conjecture.
Read this published revision