把论文、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+ 上表现不好，我们得到的是「一定存在一个没人想掀桌子的委员会」——但那个委员会未必代表少数派。
存在性和公平性，是两件事。