ℚ₂ 的绝对 Galois 群的显式表示

AI 模型给出了 2-进数域绝对 Galois 群的一个候选显式表示，这是唯一尚未解决的情形；已有 Lean 形式化，但依赖于引用的文献结果，相关文稿也未经同行评审。

问题
用生成元和关系给出 Q2\mathbb{Q}_2 的绝对 Galois 群的显式表示。
贡献方
Claude Fable 5（据 Epoch AI）与 GPT-5.5 Pro，以及 David Roe、David Turturean · 由人引导 AI 得到解答
验证
两个依赖引用结果的 Lean 形式化Epoch AI 标记为已解决
时间线
Claude Fable 5 的解答 2026-06-09 → GPT-5.5 Pro 的解答 2026-06-24 → 文稿 2026-07-26
来源
Epoch AI 问题页面Roe 与 Turturean 的文稿
待核实Lean 依赖外部结果 · 未经同行评审

问题

一个域的绝对 Galois 群同时编码了它的所有有限扩张。对于 p>2p > 2 的 pp-进数域 Qp\mathbb{Q}_p，人们已经知道用生成元和关系给出的显式表示；p=2p = 2 的情形一直未解决。

AI 做了什么

据 Epoch AI 介绍，这个问题最早由 Claude Fable 5 在 David Roe 主持的一次会话中解决（2026 年 6 月 9 日），David Turturean 随后在 6 月 24 日借助 GPT-5.5 Pro 也得到了解答。但 Roe 和 Turturean 的文稿（2026 年 7 月 26 日）给出的说法不同：文稿称是一次 ChatGPT Pro 会话找到了候选表示和一个非形式化的证明。

如何验证

目前有两个 Lean 4 形式化：一个以 9 个引用自文献的结果作为接口，另一个依赖 7 个外部输入。Epoch AI 的验证程序在 5,402 个测试群上与预测的扩张个数一致，Epoch 认为这是强有力的证据，但不是证明。

局限

这篇文稿未经同行评审，也没有存档编号；形式化证明依赖于从文献中引用的结果；各方对究竟是哪个模型找到了这一表示说法不一。我们暂时将其记为"待核实"。问题描述转述自 Epoch AI（CC BY 4.0）。

∎