和谐人工智能自主解决了4个有30年历史的数学难题

Harmonic AI，解决4个30年数学难题：AI数学时代开启

数学 AI 初创公司 Harmonic 开发的 Aristotle AI 在 2026 年 1 月的一个月内连续解决了 4 个未解决的埃尔德什问题。^[arXiv] 埃尔德什问题是传奇匈牙利数学家保罗·埃尔德什留下的 1,133 个难题的集合。其中 680 个仍未解决。

最值得关注的成果是问题 #728。1 月 4 日，凯文·巴雷托利用 Aristotle 发表了证明，1 月 6 日，使用 Lean 4 编程语言完成了形式验证。^{[Hacker News]} 这是 AI 在没有人类帮助的情况下完全自主解决埃尔德什问题的首例。

随后，问题 #729、#397 和 #124 依次得到解决。问题 #124 自 1990 年代以来一直未解决，长达 30 年，但 Aristotle 仅用了 6 个小时就解决了。^[36Kr]

AI 解决数学问题并不新鲜。DeepMind 的 AlphaEvolve 在 50 多个数学难题中也取得了优于人类的结果。但 Aristotle 的区别在于形式验证。

现有的 LLM 会给出看似合理的答案，但无法避免幻觉。Aristotle 通过 Lean 4 证明辅助器生成数学上完美的证明。菲尔兹奖得主陶哲轩在一天内审查并批准了问题 #397 的证明，也得益于这种可验证性。

Harmonic 在 2025 年 11 月的 C 轮融资中以 14.5 亿美元的估值获得了 1.2 亿美元的投资。2026 年 1 月，Nvidia 的 NVentures 也加入了投资者行列。^{[SiliconANGLE]}

Harmonic 的联合创始人弗拉德·特内夫（Robinhood CEO）和都铎·阿基姆的目标是数学超智能。数学验证技术有望扩展到编码、芯片设计和安全关键软件验证。

但陶哲轩警告说，目前解决的问题是最容易摘取的果实。这些问题可以用标准技术解决，与真正的数学突破相去甚远。AI 在问题框架和专家验证方面仍然依赖于人类。

Q: Aristotle AI 是如何解决数学问题的？

A: Aristotle 结合了强化学习、蒙特卡洛树搜索和 Lean 4 形式语言。它将自然语言的数学问题转换为形式上可验证的证明。GPT-5.2 生成初始证明后，Aristotle 会以 Lean 进行形式验证，从而进行协作。

Q: Harmonic AI 是一家什么样的公司？

A: 这是一家成立于 2023 年的帕洛阿尔托初创公司。Robinhood CEO 弗拉德·特内夫是联合创始人兼董事会主席，都铎·阿基姆是 CEO。在 C 轮融资中获得了 14.5 亿美元的企业估值，Nvidia、Sequoia 和 Index Ventures 进行了投资。

Q: 什么是埃尔德什问题？

A: 这是匈牙利数学家保罗·埃尔德什一生提出的数学难题的集合。目前已编目 1,133 个，其中 279 个已解决，680 个未解决。涵盖了数论、组合论、图论等多个领域。

如果这篇文章对您有帮助，请订阅 AI Digester。