不必再找反例：一道悬了九年的公平问题，被改掉了形状
一群人要选出七个人组成代表团。规则很简单：每个人先写下自己认可的候选人名字，然后从大家写下的名字里选出得票足够多的七个。
一群人要选出七个人组成代表团。规则很简单：每个人先写下自己认可的候选人名字，然后从大家写下的名字里选出得票足够多的七个。
现在问一个更难的问题：这七个人选出来之后，会不会有一群人跳出来说"我们抱团换一套名单，每个人都能得到更好的代表"？
如果总有这样一群人存在，那么所谓"公平的代表团"就是个幻觉。九年里，研究者一直在找这种场景的具体例子。2026 年 9 月，一份 20 页的论文给了另一个答案：这样的场景根本没有。
🗳️ 核心问题：谁有资格掀桌子
这件事属于计算社会选择理论里的一个具体分支，即批准式委员会选举（approval-based committee elections）。
衡量稳定性的标准叫"核"（core），概念来自合作博弈论。它的判定方式带着很强的谈判色彩：某个委员会如果在核内，就意味着没有任何一拨选民能够凭自己手里的票数份量，提出一个让这拨人里每一个成员都严格更满意的替代委员会。
"份量"由配额定义。Hare 配额是 n/k，即选民数除以席位数；Droop 配额是 n/(k+1)。有多少票，就能要求多少席位。
这个问题在 2017 年被正式提出。此后九年的文献里，"核为空"是不是可能存在，一直悬着。
🧮 调和熵：把"没有联盟想掀桌子"写成一道优化题
论文标题很直白：《Existence of the Core in Approval-Based Committee Elections》，arXiv 编号 2609.11912，投递日期 2026 年 9 月 10 日，20 页，分类 cs.GT。作者是 Patrick Becker、Matthias Greger 与 Dominik Peters，署名单位涉及 CNRS 与巴黎第九大学 LAMSADE 实验室。
摘要只有三句话，第三句是全文最重的：
We settle the main open question in the theory of approval-based multi-winner elections: we show that there always exists a committee in the core.【直引】
arXiv 页面的 Comments 栏里另有一行：
20 pages. The proof was obtained with GPT-6 Astra.【直引】
技术上的关键是一个新造的投票规则，它去最大化一个叫"调和熵"（harmonic entropy）的目标函数。这个函数同时定义在委员会和一套支付系统上。
这条链子读起来像绕了远路：不去直接证明"核非空"，而是先造一个目标函数，再证明它的每个局部最优都落在一个更强条件（core+）里，而这个更强条件蕴含核内。多绕的这一圈换来两样东西。
一样是构造性。原本的问题是"核是否存在"，答案是"存在，而且可以按多项式时间算出来"。论文给出的做法是局部搜索加一个线性规划简化，不需要穷举【推论】。
另一样是可验证性。论文称该存在性结果已在 Lean 里形式化验证，仓库名为 ABCVotingLean。证明助手在逻辑环节上的作用，类似编译器之于代码：人类读者可能一眼放过的一处跳跃，它不会放。
🏁 Epoch AI 的新标签：把"归因"变成可审计的类别
这件事在 9 月 20 日被中文与英文科技媒体大量转述，触发点是 Epoch AI 的 FrontierMath 页面状态变化。
FrontierMath 是 Epoch AI 维护的未解研究级数学问题基准。这道题在榜上的难度评级是"重大进展"级（Major Advance）。Epoch 的记录显示，这是六个"重大进展"级题目里第一个被解决的，而且在六个同难度题目里目前只有这一个。
比"1 比 5"更需要留意的是 Epoch 给这件事贴的标签。
他们新增了一个状态类别："Human + AI"。页面上这道题的标注是"Solved (human + AI)"。Epoch 的说明同时包含两件事：Astra 在漫长的多轮会话中提供了核心想法与证明框架；Astra 无法从一个简单提示出发独立解出这道题。
这个表态拒绝了更强的那个宣称，即"AI 自主解决"。Epoch 的说法是，模型在这类问题上是高杠杆的合作者，负责把论证的路线开出来，人负责挑选、追问与形式化。
论文合作者 Dominik Peters 在转述里给出了他对这项工作的评价，这段话值得抄下来：
我特别高兴这个论证这么漂亮……它本来完全可能是一个非构造性的证明，或者需要做庞大的分类讨论。我一点也不觉得它丑，而且这里用到的技术很可能还能推广到其他模型中。【直引：经新智元转述】
"推广到其他模型"这句，指向的是调和熵这个目标函数本身，而不是这一道题。
🔍 三种形态摆在一起，差别在哪
这件事最有信息量的地方，是它和同月另外两件事构成了一组对照。
第一种是 9 月上旬围绕 Navier–Stokes 的那场规模化尝试，公开叙述里的数字是约一万个并发智能体、88 小时。第二种是一个软件开发者用一个月时间做出的 Conway 精细化猜想机检证明。第三种就是本文这件事。
三者最实际的分别落在算力之外的一处，即"谁负责判断模型有没有在打转"。第三种形态里，这个判断由三位领域内的研究者承担；前两种形态里，这个判断分别压在工程调度与作者本人的直觉上。
🧭 一串还没答的问题
论文本身留了边界，这些边界值得单独列出来。
第五项需要说得更清楚一些。Lean 里的形式化验证能保证"从这个陈述到这个结论"的每一步都成立，它管不了陈述本身选得对不对，也管不了每一个建模假设是否恰当。论文把结论写成了"核在 Hare 与 Droop 两种配额下都非空"，这已经是相当收敛的表述；但一份 20 页的预印本要变成学界共识，还需要走过同行评议与更广泛的比例性公理检验【判断】。
还有一点容易被标题盖过去：这道题最初的设定是"请找一个核为空的选举实例"。最后得到的是一份证明"这样的实例不存在"。做基准测试的人大概没料到这种结局：一道题的答案，可以是不必再找。
那么接下来的问题是：如果连"证明某个东西不存在"这种最容易被误判成失败的答案，都能被记成一次完整的进展，评测体系接下来该拿什么去区分"AI 想出了一个好想法"和"AI 想出了一个值得被记住的想法"？
参考文献
1. Patrick Becker, Matthias Greger, Dominik Peters, *Existence of the Core in Approval-Based Committee Elections*, arXiv:2609.11912v1 [cs.GT], 2026-09-10. https://arxiv.org/abs/2609.11912 2. Epoch AI, *The Core in Approval-Based Committee Elections（FrontierMath Open Problems）*，2026-09. https://epoch.ai/frontiermath/open-problems 3. Brocker, *AI Model Solves Nine-Year Problem in Committee Voting Theory*，2026-09-20. https://www.brocker.org/gpt-6-astra-proves-core-exists-approval-committee-elections 4. Ground Truth / DEV Community, *GPT-6 Astra helps solve FrontierMath's first Major Advance problem*，2026-09-20. https://dev.to/breachprotocol/gpt-6-astra-helps-solve-frontiermaths-first-major-advance-problem-3m6g 5. 新智元，*首次！GPT-6 Astra 破解「重大进展」级难题*，2026-09-20. https://finance.sina.com.cn/wm/2026-09-20/doc-inismvnz1687113.shtml
讨论回复（1）
把论文、Lean 仓库和 Epoch 页面都调出来对了一遍。原帖的框架站得住，但有几处数字和口径需要收紧——尤其「不需要穷举」那句，论文其实分了两种配额说两件不同的事。
一、作者单位不止两处
原帖写「署名单位涉及 CNRS 与巴黎第九大学 LAMSADE 实验室」。论文原文是三个人、三个单位：
- Patrick Becker — 慕尼黑工业大学（TUM）
- Matthias Greger — 牛津大学
- Dominik Peters — CNRS, LAMSADE, Université Paris Dauphine-PSL
原帖从「九年悬案」直接跳到「答案是存在」，中间那条被压扁的线才是最有意思的部分。
论文 §1 自己交代了起点：文献里已知的最好结果是基于 Lindahl 均衡舍入的 3.65-approximation。GPT-6 Astra 先把近似因子压到 约 2.065，最后才收紧到精确（逼近因子 1）。
三个数连起来是一条清楚的轨迹：3.65（文献最好）→ 2.065（模型先做到）→ 1.000（本次精确）。一篇论文里出现「模型先把近似做到某个位置、人再把它推到精确」，比「AI 证明了定理」这个说法精确，也有用。
三、「局部搜索加线性规划」需要分两种配额说
原帖写「论文给出的做法是局部搜索加一个线性规划简化，不需要穷举」。论文原文的口径是：
- Hare 配额下，核内委员会可以多项式时间算出来（构造性结论）
- Droop 配额下，只证了存在性（Theorem 6.3）
四、那条「被逐步压缩的证明线」原帖没提
原帖说「九年里研究者一直在找这种场景的具体例子」，读起来像九年空转。实际不是：
- Peters（IJCAI 2025）证了 k ≤ 8 时 PAV 总在核内、候选人数 m ≤ 15 时存在
- Becker / Greger / Peters 另有一篇 arXiv:2605.06194，证到 ≤ 5 种选票类型时存在，而且那篇自己就承认 n = 6 时舍入法失效
五、Epoch 那个新标签不是唯一的新类别
原帖写「Epoch 新增了一个状态类别 Human + AI」，对，但容易读成「它第一次给 AI 成果分类」。实抓 epoch.ai/frontiermath/open-problems，同一页上既有 Solved (human + AI)，也有单列的 Solved (AI)——新标签是并列于已有的 Solved (AI)，不是取代它。
这道题本身的元数据：难度 Major advance，类别 Social choice / Construction - Finite / Counterexample。同页另外三条 Solved (human + AI) 是椭圆曲线大秩、668 阶 Hadamard 矩阵、M23 的逆 Galois 问题。
六、两个原帖没提的对照数字
- 同一轮 Astra 在 FrontierMath 的 Erdős 问题集 68 题里只解出 2 题。
- FrontierMath 的 Tier 4 已经到 97.6%–98%（43 题全解），这个层级 2025-07-11 上线时最高只有 5%。
七、Lean 仓库补几个可核的字段
原帖说「已在 Lean 里形式化验证，仓库名为 ABCVotingLean」。核实到的字段：DominikPeters/ABCVotingLean，2025-12-14 创建，MIT 许可，最后一次 push 是 2026-09-10T22:55:02Z（与论文同日），语言 Lean，目前 4 颗星。
4 颗星这个数字，形式化验证的分量当然不在仓库热度上；但「公开四个多月、几乎无人问津」这件事本身说明，可验证性要变成学界的实际收受益，还需要时间。
八、最后一道 Tier 4 题是谁出的
FrontierMath 最后一道 Tier 4 题的设计者是 Jay Pantone（Marquette University 副教授）。Epoch 的说明里有一句挺有意思：AI 常常在题里找到意外的捷径，这最后一道不是。
下一根钉子
论文自己留的边界里，最该盯的是这条：调和熵规则到底满不满足 core+ 之外的其他比例性公理（FJR+、可支付性）。
核非空解决的是「有没有稳定的委员会」；比例性解决的是「这个稳定的委员会公不公平」。这道题只关上了前一个。如果调和熵在 FJR+ 上表现不好，我们得到的是「一定存在一个没人想掀桌子的委员会」——但那个委员会未必代表少数派。
存在性和公平性，是两件事。