※ 引述 《Bugquan (靠近边缘)》 之铭言： : 推 LPH66 : 话说回来, 我看到有一篇论文是他们用 ChatGPT 产生 11/06 20:35 : → LPH66 : 了 Lean 程式码并且成功编过了, 这种应该算是生成式 11/06 20:36 : → LPH66 : AI 的一种意外应用方式吧 (Lean 程式码能编过表示 11/06 20:36 : → LPH66 : 逻辑推理是通的) 11/06 20:36 : → LPH66 : 这篇论文的作者有说他们在这之前不会 Lean 11/07 08:52 https://xenaproject.wordpress.com/2025/10/22/formal-or-not-formal-that-is-the-qu estion-in-ai-for-theorem-proving/ 根据 Kevin Buzzard（伦敦帝国学院教授，https://reurl.cc/LQ0Ddx）的观点，我们来探 讨 AI 证明数学猜想时的核心问题。 小知识：关於 Kevin Buzzard 这位数学家正带领团队，试图利用 Lean 形式化证明费马最後定理。他甚至邀请到他的指导 教授 Richard Taylor（费马最後定理证明关键贡献者之一）来协助制定一套现代化且更具 可行性的形式化蓝图。 (参考：https://imperialcollegelondon.github.io/FLT/blueprint/) Kevin Buzzard 在文章中指出，AI 证明数学时面临两大挑战： 1. AI 的「幻觉」与证明可靠性 问题核心： 像大型语言模型（LLM）这样的 AI 存在「幻觉」（Hallucination）问题。 在数学证明中，只要证明过程出现一个幻觉，就足以完全破坏整个数学论证的有效性。 形式化的作用与局限： 如果我们要求 AI 在提供证明的同时，也以 Lean 形式化语言呈 现，是否就能高枕无忧？ 答案是否定的。 虽然 Lean 可以以超人类水平校验逻辑步骤，但人类仍然需要仔细检查 ：定理的陈述和证明的过程是否被正确地翻译成了 Lean 语言。 确保「人类想证明的」与「Lean 实际检查的」是同一件事，是至关重要的环节。 2. AI 配合 Lean 的发展瓶颈 问题核心： AI 与 Lean 混合系统能走多远？ Buzzard 的观点： 他认为目前的瓶颈在於，即便是最好的形式化数学函式库（如 Lean 的 mathlib），仍不具备理解大多数现代研究级数学所需的「定义」。 范例： 目前的定理证明器尚不了解（或缺乏足够形式化定义）这些复杂但又极其重要和 常用的数学对象，例如： Tate-Shafarevich 群 Calabi-Yau 簇 代数叠 (algebraic stacks) 自守表示 (automorphic representations) 因此，在 AI 能够真正协助进行研究级数学证明之前，仍需要人类研究人员投入时间，为 L ean 等证明器提供和形式化这些现代数学的基础定义。 --

※ 发信站: 批踢踢实业坊(ptt.cc), 来自: 27.53.161.22 (台湾) ※ 文章网址: https://webptt.com/cn.aspx?n=bbs/Math/M.1762480024.A.346.html