The 26×26 queen domination number is 14. Now proved in Lean.

The open question was whether 13 queens could dominate a 26×26 chessboard. Official problem/reference page: https://oeis.org/A075458

A working arrangement with 14 queens was already known.

The new Lean proof establishes both sides:

14 queens can dominate the board. Every dominating set needs at least 14 queens.

Queens may attack each other, so this is the ordinary queen domination problem -- not the stricter nonattacking version.

The earlier SAT search did not return UNSAT and remains marked UNKNOWN. This is a separate mathematical proof checked by Lean 4.32.2 and the independent nanoda kernel. I set out to figure out a different way to work on this since the SAT search was taking enormous emounts of space/time/soul.

I may have 7 years to search but my computer was getting hot.

I used ChatGPT 5.6 Sol Ultra for theorycrafting, and Codex for the implementation/python/coding/Lean. Mostly I asked it to look at the existing solutions, and try to devise new algorithms and ways of solving it that didn't try to play by the pre-existing routes.

Readable proof: https://github.com/jkolantree/BSC/blob/main/applications/Q26_Color_Split_Grid_Annihilator_Proof.md

Final Lean theorem

Independent validation

Implementation and validation