核心事件 - AI数学家“亚里士多德”在6小时内，100%独立破解了30年未解的埃尔德什问题124的简化版本，验证仅需1分钟，全程无人类辅助，被形容为数学界的“登月”时刻 [1][2][4] - 该AI由HarmonicMath公司开发，结合了强化学习、蒙特卡洛树搜索和Lean形式化语言，通过搜索上亿种证明策略输出可验证定理 [11][13] - 菲尔兹奖得主陶哲轩高度赞扬了这一成就，并指出数学界正迎来“vibe证明”的时代 [4][5][6] 技术突破细节 - 解决的问题是埃尔德什问题列表中的第124号问题，该问题在论文“Complete sequences of sets of integer powers”中提出，核心是探究在极端约束下是否总能用“二进制”表示任意大数 [7][9] - AI“亚里士多德”输出的定理形式化为：theorem erdos_124 : ∀ k, ∀ d : Fin k → ℕ, (∀ i, 2 ≤ d i) → 1 ≤ ∑ i : Fin k, (1 : ℚ) / (d i - 1) → ∀ n, ∃ a : Fin k → ℕ, ∀ i, ((d i).digits (a i)).toFinset ⊆ {0, 1} ∧ n = ∑ i, a i [13] - 目前解决的是该问题两个版本中较为简单的一个，完整版本更具难度 [14][22] 行业影响与趋势 - 陶哲轩指出，数学未解问题服从“长尾分布”，AI自动化正在收割长尾末端的“低垂果实”，即大量相对容易但因关注度低而未解决的问题 [16][18] - 近期，埃尔德什问题网站的“未解”标签下减少了近十个问题，均因AI辅助的文献搜索发现已被解决，人类数学家也正结合AI工具和形式化证明助手进行研究 [20] - AI自动化工具能先清理容易的问题，将真正困难的部分剥离出来，使人类数学家能更专注于值得投入的难题 [23] 竞品对比 - 根据陶哲轩的点评，Gemini和ChatGPT的深度研究工具均未能针对该问题找到新的、有价值的文献 [15] - Gemini仅给出了一个简单的观察，并将其与一些平行研究联系起来，但未找到直接相关的新文献 [15] - ChatGPT大量依赖现有网页作为权威来源，未能提供新信息，尽管其生成的总结可能有趣 [15] 应用案例与前景 - 陶哲轩以“Equational Theories Project”为例，该项目涉及普遍代数中2200万条可能的蕴涵关系，通过采用自动化方法在几天内解决了大部分，仅剩的顽固难点最终由人类数学家花费数月攻克 [18] - AI发现另一类“低垂果实”是因描述存在技术性瑕疵而意外变得好解决的问题，E124的简化版本即属此类，其因遗漏关键假设而成为已有判据的直接推论，这一漏洞由AI自主发现并证明 [21][22][23] - 埃尔德什问题网站收录了1108个问题，其中包含大量不起眼、几乎无人关注的问题，为AI自动化攻克提供了广阔空间 [20]