6小时破30年数学难题，AI版“亚里士多德”一夜成名。社交媒体上已经吵翻了——Harmonic的数学AI模型，用6小时独立证明了Erdos问题 124（简易版），而这个问题被数学界搁置了近三十年。消息最先由微软前AI副总裁、现OpenAI AGI研究员Bubeck公布，陶哲轩也亲自下场围观，甚至和Gemini、ChatGPT 的深度研究工具对比了一下，结论是：这题Harmonic模型证明得更好。不过补一句：它证明的不是严格原版，而是简化版。原题要求更严（不能用 1，还要满足gcd条件），三十年来只在 {3,4,7} 这种特殊集合上成立。而放宽条件后（允许用 1、无需gcd），Harmonic给出了完整证明，而且已经通过Lean形式化验证。更戏剧性的是：原本的形式化项目中公式条件写错了，注释是≥1，代码却是=1，只覆盖了“刚好等于1”的情况。研究者修正后，删掉了不必要限制，AI才成功证明了这个更准确的版本。结论：难题原版依然悬着，简易版被AI拿下。但数学圈的兴奋点不在这里，而在于—— “Vibe证明时代来了。”Harmonic联创直接喊话：就像当初有了Vibe Coding，现在数学也要进入“靠 vibe 找路子”的新阶段。要知道，Harmonic这家公司才成立两年，目标就是打造“全球最强数学推理引擎”。CEO Tudor Achim是CMU/斯坦福背景，联合创始人还是Robinhood CEO Vlad Tenev。Harmonic刚刚拿下1.2亿美元C轮融资，估值14.5亿美元。他们的旗舰模型Aristotle（“亚里士多德”）已经在2025 IMO里形式化解决了5道奥赛题，这次证明124用的也是升级版Aristotle，推理能力更狠。从奥赛题，到30年数学难题，再到Lean的形式化验证，“AI证明数学”这条线，正从概念走向现实。很多数学家都在说：以前觉得AI做证明像科幻，现在开始怀疑——下一批百年难题，会不会先被AI解掉？Anyway，时代的箭已经射出去，回不来了。数学AI