2025年，AI系统Aristotle首次自主解决埃尔德什开放问题，标志数学形式化进入全自动时代。从手动验证到AI流水线，数学研究范式正在被彻底重构。
人类数学正被AI彻底重构：Erdős难题迎来“AI自动破解”时代
2025年12月初的这个冬天，一个人工智能系统在深夜自动运行数小时后，醒来就发现它已经解开了一道被传奇数学家保罗·埃尔德什（Paul Erdős）列为“开放问题”的数学谜题？
更震撼的是，这个证明不仅简洁优美，还被数学界誉为“来自《天书》”（The Book）的解法！这不是科幻小说，而是正在真实发生的数学革命。
今天这篇文章，就带你深度走进这场由AI驱动的数学形式化浪潮，看看人类如何借助大模型与形式验证工具，把百年前的猜想变成可验证、可传播、甚至可“自动生成”的数字真理。
埃尔德什的问题宇宙：1100道谜题背后的文化密码
要说清楚这一切，我们必须先回到一个名字：保罗·埃尔德什。这位20世纪最具传奇色彩的数学流浪者，一生没有固定住所，靠朋友收留、靠咖啡因驱动，发表了超过1500篇论文，合作过500多位数学家。
他不仅做研究，更热衷于提出问题——有些简单到高中生能懂，有些则深不可测。他甚至为某些问题悬赏金钱，从几十美元到几千美元不等，以此激励后人思考。
如今，在 erdosproblems.com 这个由数学家托马斯·布鲁姆（Thomas Bloom）于2023年5月创建的网站上，已经收录了超过1100道埃尔德什提出的问题。其中约40%已被解决，约240道问题的陈述已被形式化为Lean语言（一种现代定理证明语言），17个问题的完整解法也已完成形式化验证。
更酷的是，2025年8月，该网站新增了论坛功能，迅速引爆全球数学爱好者的讨论。
与此同时，谷歌DeepMind启动了“形式化猜想”（Formal Conjectures）开源项目，专门收集包括埃尔德什问题在内的各类数学猜想的形式化表述。
托马斯·布鲁姆还与菲尔兹奖得主陶哲轩（Terence Tao）联手，推动将这些猜想与“整数数列在线百科全书”（OEIS）建立链接。如今已有260多个问题成功关联至OEIS条目。这一切，正在构建一个前所未有的“可计算数学宇宙”——问题可查、解法可验、逻辑可追溯。
从零到Lean：人类如何亲手将猜想变成机器可读的证明
故事的起点其实并不依赖AI。
早在2022年，托马斯·布鲁姆与巴维克·梅塔（Bhavik Mehta）就完成了对“问题47”（关于单位分数的分解）的完整形式化。有趣的是，布鲁姆在开始时对Lean一无所知，完全是“边做边学”。
他们的工作不仅是首个被形式化验证的解析数论新成果，也是“圆法”（circle method）首次在形式系统中实现，更是首个被正式验证的埃尔德什问题解法。
他们在论文中写道：“这证明了Lean和其配套数学库Mathlib已足够成熟，能在与传统论文发表同步的时间尺度上完成新研究的形式化。”这个“证明即代码”的理念，正是当今数学形式化运动的核心精神。
此后几年，虽有零星进展——如对问题77、216及著名的哈德维格-尼尔森问题（问题508）的部分形式化——但整体节奏仍较缓慢。
直到2025年夏天，“形式化猜想”项目上线，以及 erdosproblems.com 论坛激活，才真正点燃了社区协作的火种。
例如，2025年秋季，斯汀·坎比（Stijn Cambie）、维耶科斯拉夫·科瓦奇（Vjekoslav Kovač）与陶哲轩合作解决了问题379，并“亲手”用Lean完成了形式化；几天后，陶哲轩又独立解决了问题987（事后才知埃尔德什本人早已解决），同样手动完成Lean验证。
这些早期工作虽无AI介入，却为后续爆发打下了坚实基础。
AI初登场：用ChatGPT“vibe code”出Lean证明
真正的转折点出现在2025年下半年。作者鲍里斯·阿列克谢耶夫（Boris Alexeev）与达斯汀·米克森（Dustin Mixon）合作解决了“问题707”。
在完成传统数学推导后，他们尝试了一种前所未有的方式：直接让ChatGPT“凭感觉”（vibe code）生成Lean代码。
他们在论文中坦承：“我们感觉自己正在尝试一种全新的数学研究范式——将大语言模型与形式验证结合，产出既重要又可认证正确的结果。”
这一尝试引发连锁反应。有数学家反馈，三年没碰Lean，如今再回来看，整个生态已焕然一新：Mathlib库更完善，Lean语言更友好，加上LLM辅助，形式化效率提升数倍。受此启发，陶哲轩也用类似方法，让ChatGPT辅助完成了对奥列格·皮胡尔科（Oleg Pikhurko）所解“问题613”的形式化。
值得注意的是，此时的AI还只是“辅助”——人类仍需主导逻辑结构，AI负责语法转换和细节填充。
Aristotle登场：形式化进入“自动驾驶”时代
但真正的革命，来自一个叫Aristotle（亚里士多德）的AI系统——由Harmonic公司开发，2025年中向公众开放。
最初，Aristotle只能完成Lean中的“sorry”占位符，即给定一个已形式化的定理陈述，它能尝试生成证明。
作者用它成功验证了吴锡川（Wu Xichuan）在论坛上提出的“问题105”的反例。
此前他用纯ChatGPT失败，而Aristotle一试即成。
原因很简单：该反例虽难构造，但验证逻辑极其直接。
很快，Aristotle升级了“非形式模式”（informal mode）——能直接读取用自然语言或LaTeX写成的数学文本，并自动将其转化为Lean形式化证明！
这彻底改变了游戏规则。
作者与陶哲轩、Gemini DeepThink、Wouter van Doorn等人合作，用此功能完成了“问题367”部分解法的形式化。
更疯狂的是，作者随后搭建了一个自动化流水线：人工选定一个问题 → 让ChatGPT解释其解法 → 用Aristotle将解释文本自动形式化 → 与“形式化猜想”项目中的定理陈述拼接 → 交给Lean验证 → 自动推送到GitHub，甚至自动生成论坛评论！
这套流程首次在“问题645”上完美运行。
虽然后续十几次尝试中常需人工干预（流水线仍脆弱），但效率已从“半年”缩短到“几小时”。
如今，Aristotle已贡献了 erdosproblems.com 上大多数公开的形式化解法。更重要的是，整个过程几乎“无人值守”——你提交任务，去睡觉，醒来就能看到机器给你一份可验证的数学证明。
AI自主解题：深夜醒来，发现AI已破解埃尔德什开放问题
如果说辅助形式化是“增强人类”，那么2025年12月初的事件则是“取代人类”的开端。
作者某周五晚上手动挑选了几个开放问题，启动Aristotle后就去睡觉了。第二天一早，他收到邮件：Aristotle成功解决了“问题124”！这道题出现在埃尔德什1997年出版的两本问题集中（他于1996年去世），一直被视为开放问题。
经过仔细核查，作者确认：Aristotle的证明完全正确。
尽管后来发现，埃尔德什可能本意是另一个稍有不同的版本（因此问题陈述已被修改），但就当前形式化表述而言，AI确实“首次自主解决”了一个公认的埃尔德什开放问题。更令人震撼的是，这个证明极其简洁——被众人称为“奥数级别”，但作者坚持认为，它更应被称作“来自《天书》”——埃尔德什曾说，上帝有一本记录所有最美证明的《天书》，而这个解法正配得上这份荣耀。
紧随其后，凯文·巴雷托（Kevin Barreto）在不知情的情况下重新解决了“问题481”（原解者为1982年的David Klarner），并请Aristotle完成两件事：形式化他的证明，并尝试自主求解。结果双双成功！这意味着，Aristotle不仅能复现人类解法，还能独立发现新解。多个团队随后声称也实现了对这些问题的全自动求解。
此外，谷歌DeepMind的AlphaProof系统（可直接输出Lean代码）也为社区贡献了新知：为“问题730”构造了有趣示例，为“问题198”找到了漂亮反例。虽然这些证明常需人工重写以提升可读性，且因问题陈述随后被修改，目前尚无AlphaProof生成的解法被正式归档，但其潜力毋庸置疑。
形式化的暗礁：AI也难逃“误形式化”陷阱
然而，作者也坦承：形式化之路并非坦途。他总结了三类“误形式化”（misformalization）：
低级错误：如“问题480”的形式化中误写“m ≠ 0”应为“n ≠ 0”，Aristotle竟利用此漏洞构造出反例；还有不等式方向写反、忽略平凡零解、量词顺序颠倒等。这类错误在Lean中比Python等语言更常见，因数学家对Lean不熟，且代码不“运行”而是“验证”。
缺失假设：1994年Ahlswede与Khachatrian对“问题56”的反例依赖参数212，但作者形式化时，Aristotle用参数2就找到反例——原来原猜想隐含了一个未明说的假设。补上后，证明才成立（过程中作者自己还犯了“差一错误”）。
高层误解：“问题124”本身可能就属此类——埃尔德什晚年修改问题时，无意中弱化了条件，导致问题变得过于简单。AI解出的正是这个“简化版”。
作者强调：AI工具不仅能发现低级错误，更能揭示数学家思维中的盲点。尤其是第三类，能帮我们聚焦真正核心的数学结构。
形式化不是终点，而是新协作范式的起点
所以，这一切意味着什么？
有人或许会说：埃尔德什问题多属初等问题，不具代表性。
但作者反驳道：关键在于社区力量与数据基建。
埃尔德什问题之所以成为AI试验田，是因为：
（1）全球数学家珍视这些问题，乐于讨论与协作；
（2）社区已建成高质量、双语（自然语言+Lean）的问题库。
随着更多数学领域完成形式化（即向Mathlib贡献定义与定理），同样的故事将在代数几何、拓扑、PDE等深水区上演。
作者呼吁：如果你想推动自己领域的形式化，不妨学习埃尔德什社区的经验——将你的猜想提交至“形式化猜想”项目；积极参与Mathlib建设；构建带论坛的问题数据库。因为只有当知识被结构化、可计算，AI才能真正成为你的研究伙伴。
这场变革的核心启示是：未来的数学，不仅是写在纸上的推理，更是可执行、可验证、可进化的代码。而AI，正成为连接人类直觉与机器严谨的桥梁。