Harmonic AI，解决4个30年数学难题：AI数学时代开启
- Harmonic的Aristotle AI自主解决了4个埃尔德什(Erdős)问题
- 问题 #728 是 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 在问题框架和专家验证方面仍然依赖于人类。
常见问题 (FAQ)
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。
参考资料
- Resolution of Erdős Problem #728: a writeup of Aristotle’s Lean proof – arXiv (2026-01-06)
- Harmonic AI raises $120M at $1.45B valuation – SiliconANGLE (2025-11-25)
- AI Solved 30-Year Math Problem in 6 Hours – 36Kr (2026-01-14)
