这篇论文展示了 AI 在数学证明中的实际进展，做形式化验证或数学研究的团队值得关注——它把 LLM 从“讲故事”变成“可验证的候选生成器”，直接解决了幻觉问题。
Google DeepMind 发表新论文，展示 AI 系统 AlphaProof Nexus 能在形式化数学证明中进行搜索，但仅限于精心约束的世界。该系统使用 Lean 证明检查器，让 LLM 不断编辑形式化证明、读取编译器错误并重试，同时维护共享的局部证明池来指导搜索。在测试中，该系统解决了 9 个 Erdős 问题和 44 个序列猜想，并协助优化、图论、代数几何和量子光学领域的问题。失败案例同样有启示性，揭示了 LLM 在数学推理中隐藏错误的方式。该工作并非实现完全数学自主，而是建立了人机协作的新分工：人类选择问题，模型提出路径，证明助手严格验证。
Google DeepMind's new paper. Shows that AI can no…
Google DeepMind's new paper.
Shows that AI can now search formal mathematics proofs, but only inside carefully constrained worlds.
The striking result is not that the system “thinks like a mathematician,” but that it keeps forcing its thoughts through Lean, where every step must compile.
The problem is that LLMs can sound convincing in math while still making tiny mistakes, so the authors use Lean, a proof system that checks every logical step.
Their system, AlphaProof Nexus, lets an LLM keep editing a formal proof, read compiler errors, try again, and sometimes ask a stronger proof tool for help on smaller subproblems.
The stronger version also keeps a shared pool of partial proof attempts, rates which ones look promising, and uses those attempts to guide later searches.
That changes the role of the model from a persuasive storyteller into a generator of candidates that can be killed quickly when they are wrong.
The verifier is not a cosmetic add-on, it is the mechanism that makes exploration tolerable.
Without it, a beautiful proof sketch can hide a false lemma; with it, the model has to turn insight into executable logic, or fail visibly.
The authors tested the system on real unsolved math problems, including 353 formalized Erdős problems and 492 open conjectures from the Online Encyclopedia of Integer Sequences.
The main result is that the best agent solved 9 Erdős problems and proved 44 sequence conjectures, while also helping with problems in optimization, graph theory, algebraic geometry, and quantum optics.
The failures are as revealing as the wins, because the agents sometimes buried the hard part inside a helper lemma or hallucinated a known result, exactly the kind of error formal checking is built to expose.
The real shift is not full mathematical autonomy, but a new division of labor: humans choose the formal question, libraries define the terrain, models propose routes, and the proof assistant refuses to be impressed.
----
"Advancing Mathematics Research with AI-Driven Formal Proof Search"
Paper Link – arxiv. org/abs/2605.22763