AI 如何重塑纯数学研究：从“缓慢验证”到“机器辅助”
数学中的“球体堆积问题”（如何最高效地堆叠球体）曾困扰数学家数百年，直到 1998 年 Thomas Hales 才证明了六边形堆积法的优越性。然而，为了确认这个证明无误，学界花费了超过十年时间进行逐行验证。这一现象揭示了数学界的核心瓶颈——信任。
目前，包括 DARPA 在内的多个机构正致力于利用人工智能（AI）来打破这一瓶颈，加速纯数学的发现与证明过程。
1. AI 与人类截然不同的思维方式
- 人类：倾向于制定攻击计划，有条理地书写证明过程，以便他人能跟上逻辑。
- AI：以“意识流”方式运行，基于对下一步逻辑的预测进行即兴发挥。尽管思维跳跃，但在处理长期悬而未决的数学难题时，这些模型表现出惊人的解题能力。
2. 工具与进展：让数学“自动化”
目前涌现出多种 AI 工具，旨在弥合 AI 的“即兴发挥”与数学严谨性之间的差距：
- AlphaEvolve 与 DeepThink：由 Google DeepMind 开发，利用自然语言交互帮助研究人员处理优化问题，并能解释其推理过程。
- Harmonic 的 Aristotle：能将用户提交的证明转化为严谨的 Lean 代码语言，并自动修正小错误或补全缺失的直觉跳跃，输出“无懈可击”的证明。
- Math, Inc. 的 Gauss：同样利用 Lean 语言，已成功形式化了 Maryna Viazovska 关于 8 维和 24 维球体堆积的著名证明。
3. 局限与挑战
尽管进展迅速，但人类目前仍具有核心优势：
- 缺乏跨学科的创造力：AI 难以将一个领域学到的经验灵活应用于另一个领域。
- 缺乏“美学感”：AI 难以像数学家那样追求更简洁、优美的证明，而这种审美往往是突破性发现的关键。
- 不稳定性：如 Claude 等模型在面对特定复杂问题时，偶尔会出现“胡言乱语”或逻辑崩溃的情况。
展望
DARPA 希望构建一套系统，能够将目前混乱的论文、教材和人类思维统一转化为计算机可理解的严谨语言。如果能够克服当前 AI 在逻辑稳定性和创造力上的缺陷，AI 不仅能验证现有的证明，更可能通过挖掘庞大的数学文献库，发现人类尚未察觉的逻辑联系，从而开启数学研究的新纪元。
正如专家所言，未来的挑战将不在于如何解决难题，而在于人类如何找到真正值得挑战的下一个目标。