6小时告破30年数学难题，亚里士多德一夜成名

Harmonic公司的AI模型Aristotle在6小时内独立证明了Erdős问题#124的简易版本，该版本允许使用数字1且无需满足gcd条件，并已通过Lean形式化验证。尽管原版难题仍未解决，但此次成果引发学界关注，陶哲轩等人认为其表现优于主流大模型。Aristotle此前已在国际数学奥赛中展现金牌实力。Harmonic近期完成1.2亿美元融资，估值达14.5亿美元，致力于打造先进数学推理引擎，标志着AI在复杂数学证明领域的持续突破。
来源：https://mp.weixin.qq.com/s/xIscXq4y3gFGHT-Ny5GY_Q