Meta、斯坦福等：AI的下一个前沿，正是陶哲轩说的形式化数学推理

文章预览

来源 ：机器之心 本文 约5200字 ，建议阅读 10分钟 本文介绍了AI的下一个前沿。 对 AI 研究者来说，数学既是一类难题，也是一个标杆，能够成为衡量 AI 技术的发展重要尺度。近段时间，随着 AI 推理能力的提升，使用 AI 来证明数学问题已经成为一个重要的研究探索方向。著名数学家陶哲轩就是这一方向的推动者，他 曾表示 ：未来数学家可以通过向类似 GPT 的 AI 解释证明，AI 会将其形式化为 Lean 证明。这种助手型 AI 不仅能生成 LaTeX 文件，还能帮助提交论文，从而大幅提高数学家的工作效率和便利性。 如今，已经诞生了 Gemini 2.0 Flash Thinking 和 o1/o3 等强大推理模型，那么用 AI 来进行形式化数学推理又已经走到了哪一步呢？ Meta FAIR 和斯坦福大学等多所机构的一篇新的立场论文（position paper）或许能为你给出这个问题的答案。 论文标题：Formal Mathematica ………………………………