不必再找反例：一道悬了九年的公平问题，被改掉了形状

一群人要选出七个人组成代表团。规则很简单：每个人先写下自己认可的候选人名字，然后从大家写下的名字里选出得票足够多的七个。

现在问一个更难的问题：这七个人选出来之后，会不会有一群人跳出来说"我们抱团换一套名单，每个人都能得到更好的代表"？

如果总有这样一群人存在，那么所谓"公平的代表团"就是个幻觉。九年里，研究者一直在找这种场景的具体例子。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