相关动态
Hexagon 是面向数学与理论计算机科学的新论文仓库，由多人自 2026 年 8 月初起合作筹建。作者认为借助 LLM 证明的结果大量涌现，需要新的收集模式：成果可被引用、可长期可靠保存，作者与社区参与门槛低于 arXiv，并为这些工作提供区别于 GitHub 仓库或 X/Bluesky/Mathstodon/LinkedIn 帖文的归属地。为支持项目，团队在特拉华州成立 Hexagon Mathematics Foundation，并拟申请 501(c)(3) 免税资格，作者出任首任执行主任。他举例说，与 FRG 资助团队合作时点击按钮即得到特征零四重子 Hodge 数的导出不变性这一新结果，他不愿署名而只在博客披露，如今该结果以 hexagon:2609.00104 收录于 Hexagon。
Anthropic 表示，他们分享了费马大定理的首个完整计算机验证证明。Claude 在 11 天内基本自主地用 Lean 编程语言写出证明，期间生成 1300 万行 Lean，并证明 29,500 个中间定理。费马约在 1637 年提出：对任意 n > 2，不存在正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ。Andrew Wiles 爵士 1995 年的首个证明长达 129 页。此后，包括伦敦帝国理工学院 Kevin Buzzard 于 2024 年发起的多年社区努力，推动用 Lean 证明助手完成形式化。Anthropic 研究员 Tianyi Peng 所在的哥伦比亚大学团队构建 AI 形式化工具；他测试 Claude 能否推进 FLT 形式化，结果超出预期。Buzzard 称，这项自动形式化成就证明 FLT 时除数学公理外没有其他假设，并显示 AI 自动形式化产物已足够稳健、可被继续构建。
作者参加了一场关于数学与AI的研讨会，会上产出了《莱顿宣言》，已有3000多人签署。作者虽未签署，但并非反对，而是对宣言中一些自信的断言和建议感到不确定。他强调宣言在聚焦数学界面临AI问题上的积极作用，并引用了宣言中关于数学研究特征性价值的段落，包括证明的最高确定性、归因性、透明性和独立验证性等。
在形式化与AI工具的交汇处，反例成为焦点。2026年5月20日，ChatGPT反驳了离散几何中的Erdős单位距离猜想，人类数学家虽经核查但未在Lean中形式化。五天后，Logical Intelligence（由Turing奖得主Yann LeCun共同创立）将其自动形式化于Lean中。该证明依赖Golod-Shafarevich定理，该定理的证明需100多页且涉及全局类域论，目前全局情形尚未形式化。Buzzard的学生Edison Xie正在完成局部情形的PhD项目。
“Formalizing Fermat”工作坊将于2026年7月6日至10日在伦敦举行，目标是推进EPSRC资助的、在Lean中形式化费马大定理的项目。组织者称，项目最初设想是把FLT化归到1980年代已知定理，即形式化Wiles/Taylor–Wiles论文；实际路线则是更现代、思路可追溯至Khare策略的证明。组织者刚完成11讲相关课程，并将与数论/Lean专家及自动形式化专家合作，试验AI能否形式化所需前提乃至核心证明思想。他认为自动形式化虽有进步，但尚不能可靠地自主形式化定义或定理陈述；定义密集的复杂部分可能效果差，而mathlib中定义齐备、人类文献记录充分的部分可能效果好。
本客座文章由Boris Alexeev撰写，介绍围绕Erdős问题的近期进展，特别是利用人工智能对旧新数学进行形式化。背景：保罗·埃尔德什提出了大量猜想，Thomas Bloom于2023年5月建立erdosproblems.com跟踪进展。2025年8月添加论坛，2025年5月Google DeepMind启动形式化猜想项目。Bloom和陶哲轩提议将网站与OEIS链接。目前网站上有1100多个问题，约40%已解决，约240个问题在Lean中形式化，17个有形式化解，260个链接到OEIS。文章还提及人类无AI形式化的早期例子，如Bloom和Mehta形式化单位分数问题。
计算机证明数学正处于有趣时期。对于计算机能否自主证明研究级数学定理，作者持不确定态度，但更看好AI成为数学家的有用助手，正如其当前用Lean教授研究级定义和证明的工作。就IMO问题而言，有四种公开尝试：两种用语言模型写英文证明（非形式化），两种用语言模型与Lean混合（形式化）。作者担忧非形式化方法：期刊收到越来越多由LLM生成的看似合理的论文，且有时未披露使用，并列举LLM论文与人类论文的差异，如LLM倾向于迎合。