English(EN) The 26×26 queen domination number is 14. Now proved in Lean.

AI辅助证明确认26x26棋盘支配需要14个皇后

作者 PulseAugur 编辑部 · [1 个来源] · 2026-08-12 03:33

一项数学证明解决了26x26皇后支配数问题，确定14个皇后足以且必需支配该棋盘。该证明由Lean 4.32.2和独立内核验证，是利用AI工具进行理论构建和实现的。该问题涉及皇后互相攻击，此前是一个悬而未决的问题，已知存在13个皇后的布局，但最低要求未知。 AI

影响展示了AI在解决复杂数学问题和验证证明方面的效用。

排序理由该集群描述了一个通过形式化方法验证的数学证明，这是一个研究里程碑。[lever_c_demoted from research: ic=1 ai=1.0]

AI 生成摘要 · Google Gemini · 来自 1 个来源。我们如何撰写摘要 →

报道来源 [1]

r/OpenAI TIER_2 English(EN) · /u/brain-out-of-order · 2026-08-12 03:33

26×26 王后控制数是 14。现在已在 Lean 中证明。

<div class="md">The open question was whether 13 queens could dominate a 26×26 chessboard. Official problem/reference page: <a href="https://oeis.org/A075458">https://oeis.org/A075458</a> A working arrangement with 14 queens was already known.</p…