26×26 퀸 지배 수(queen domination number)는 14입니다. Lean으로 증명 완료.
The 26×26 queen domination number is 14. Now proved in Lean.
핵심 요약
26×26 체스판의 퀸 지배 문제가 Lean 정형 증명 도구를 통해 14로 최종 확인되었습니다.
- 수학적 증명 — 26×26 체스판에서 14개의 퀸이 필요함을 Lean으로 증명함
- 도구 활용 — ChatGPT와 Codex를 사용하여 기존 방식과 다른 알고리즘을 설계함
- 독립적 검증 — Lean 4.32.2 및 nanoda 커널을 통해 결과의 정확성을 검증함
26×26 체스판을 13개의 퀸으로 지배할 수 있는지에 대한 미해결 문제가 있었습니다. 공식 문제/참조 페이지: https://oeis.org/A075458
14개의 퀸을 배치하는 방법은 이미 알려져 있었습니다.
새로운 Lean 증명은 양쪽 모두를 확립합니다:
14개의 퀸으로 체스판을 지배할 수 있습니다. 모든 지배 집합은 최소 14개의 퀸이 필요합니다.
퀸은 서로 공격할 수 있으므로, 이는 일반적인 퀸 지배 문제이며 더 엄격한 비공격 버전이 아닙니다.
이전의 SAT 탐색은 UNSAT을 반환하지 않았으며 여전히 UNKNOWN으로 표시되어 있습니다. 이는 Lean 4.32.2와 독립적인 nanoda 커널로 검증된 별도의 수학적 증명입니다. SAT 탐색이 엄청난 공간/시간/정신력을 소모하고 있었기 때문에 다른 방식으로 작업해 보기로 했습니다.
탐색에 7년이 걸릴 수도 있었겠지만 컴퓨터가 너무 뜨거워지고 있었습니다.
이론 구성을 위해 ChatGPT 5.6 Sol Ultra를 사용했고, 구현/파이썬/코딩/Lean에는 Codex를 사용했습니다. 주로 기존 솔루션을 살펴보고, 기존 경로를 따르지 않는 새로운 알고리즘과 해결 방법을 고안하도록 요청했습니다.
읽기 쉬운 증명: https://github.com/jkolantree/BSC/blob/main/applications/Q26_Color_Split_Grid_Annihilator_Proof.md
