AI数学证明突破 - Harmonic的数学AI模型独立证明了Erdős问题 124的简易版本，该问题已悬置近30年[1] - 解决方案100%由AI生成，总计耗时6小时[3] - 顶尖数学家陶哲轩对比发现Harmonic模型在该问题证明上表现优于Gemini和ChatGPT的深度研究工具[4] 数学问题细节 - 原版Erdős问题 124证明要求为∑(1/(dᵢ-1))≥1，且不允许使用数字1并需满足gcd条件，仅对特定集合{3,4,7}部分解决[8] - Harmonic证明的简易版本允许使用数字1且不需要gcd条件，只要满足∑(1/(dᵢ-1))≥1就能凑出所有大整数，证明已获Lean形式化验证[8] - 证明过程中修正了形式化猜想项目中的一个笔误，将条件从=1改为≥1，使表述更准确[10][11] Harmonic公司背景 - 公司目标为打造世界上最先进的数学推理引擎[16] - 两位联合创始人为CEO Tudor Achim（卡内基梅隆大学计算机科学学士、斯坦福大学计算机科学PhD在读）和执行主席Vlad Tenev（斯坦福大学数学学士、加州大学洛杉矶分校数学硕士）[17][18][21] - Vlad Tenev同时兼任金融公司Robinhood Markets的CEO[22] - 公司约一周前完成1.2亿美元（约合人民币8.5亿）C轮融资，由Ribbit Capital领投，估值达14.5亿美元（约合人民币103亿）[23][24] 技术能力 - 旗舰模型Aristotle（亚里士多德）是第一个在2025年国际数学奥林匹克竞赛中给出五道题形式化验证解决方案的模型，达到金牌级别表现[24][25] - 此次使用的Aristotle模型经过更新，具有更强大的推理能力和自然语言界面[26] - 公司联创称数学领域正处深刻变革边缘，"Vibe证明时代已经到来"[15] 行业影响 - AI解决复杂数学问题的能力不断突破，有望攻克更多被搁置的百年难题[27] - 此次证明展示了AI在数学推理领域的巨大潜力，引发行业广泛讨论[14]