标签
一篇纪念希尔伯特纲领提出一百周年的反思性文章，回顾了哥德尔不完备性定理和图灵停机问题如何使这一纲领受挫，并论证如今由 Lean 等证明助手驱动的 AI 智能体正在实现希尔伯特的“证明机器”，对数学和计算机科学产生深远影响。
Meta 和纽约大学的一篇新论文表明，h1 这一为模型提供快速 Lean 反馈和搜索工具的简单智能体循环，能够匹敌甚至超越人工设计的定理证明工作流：它以更低的成本在 PutnamBench 上超过了 Goedel-Architect（解出 598 题，后者为 597 题）；搭配 Opus 4.8 时，它解出了 100 道高难度代数题中的 83 道，而 Claude Code 解出了 63 道。
播客访谈：Lean 创始人 Leo de Moura 谈 AI 如何让形式化验证走向实用、验证 AI 生成代码与自主智能体的必要性，以及构建经过验证的软件栈的愿景。
本文介绍了 RefactorProof，这是一项压力测试，从 VERINA 任务中派生出 458 个经 Lean 认证的重构变体，用于衡量在保持程序行为不变的代码修改下，大语言模型生成的证明是否仍然有效。研究发现，参考证明和专用证明模型（DeepSeek-Prover-V2、Goedel-Prover-V2）均表现出显著的脆弱性，同时指出，大多数失效的证明只需少量修改即可修复。
论文提出了EasyProver——一个基于递归智能体和异步搜索的Lean证明系统，使用现成的前沿模型即可在PutnamBench和IMO基准上接近饱和；同时还提出Aegis，一个将竞赛编程转化为更具挑战性的真实世界Rust到Lean验证任务的流水线，可用于基准测试和强化学习。
提出了 PACE（研究证明代理），支持在应用数学中联合进行猜想修订与证明开发，包含研究循环、独立验证器与证据追踪记忆，并发布了聚焦优化领域的 ResearchProofBench 基准，包含 51 个已知证明任务和 6 个开放问题案例。
一篇由形式化领域顶尖研究者（Jeremy Avigad、Kevin Buzzard、Johan Commelin、Rémy Degenne、Kim Morrison、Oliver Nash、Adam Topaz）撰写的客座文章，反思了人工智能在定理证明方面的飞速进展，对仓促开展的大规模形式化项目（如 Math, Inc. 的球体填充项目以及 Anthropic 对费马大定理的验证）提出警示，并勾勒了一个由社区驱动、追求高质量的数学形式化愿景。
HOL Light 教程提供了一套循序渐进的快速入门指南，通过分级示例帮助用户快速上手 HOL Light 定理证明器，涵盖安装、OCaml 基础、项与类型、命题逻辑、重写与战术等核心内容。
该论文评估了Lean编译成功是否等同于忠实的自然语言到Lean语句形式化，发现多个系统在编译通过与语义正确之间存在1.3至29.5个百分点的显著差距，且工具增强型代理的大部分差距源于真实的翻译错误。
一篇实操性很强的博客文章，通过在 Lean、Isabelle/HOL、HOL4 和 Agda 中分别形式化欧几里得证明素数无穷性的论证，对这四个定理证明器进行了比较，并给出了关于易用性、交互性和使用体验的带有个人主见的排名。
继其大语言模型解决二十年来最大数学突破之后，OpenAI 宣布其新内部模型已再产出 372 项成果，每项都解决或大幅推进了数学或理论计算机科学中的重大公开问题，且不再需要数百万美元的成本。
Jeremy Avigad 在 Terence Tao 的博客上发表的客座文章，反思了最新 AI 能力如何颠覆数学研究的工作流程，并主张数学家必须在 AI 时代通过攻克更难的问题、追求更深的理解来做出调整。
该论文提出了 LeanPolish，这是一个符号化的 Lean 4 流水线，发布了超过 33k 条可验证的证明修改记录及失败尝试。研究表明，可验证监督数据可能存在搜索过程引入的伪影，而对符号化压缩步骤进行迭代改进，在 miniF2F 上优于神经混合方法，并在 PutnamBench 上适度提升了整体证明重写效果。
这是一篇面向软件工程师的教程式指南，在 Lean 定理证明器中形式化关于正则语言的一个构造性证明，逐步讲解规约、实现、归纳以及形式化证明的构成要素。文中展示了如何借助 Mathlib 中已有的定理，让开发者也能轻松形式化教科书中的自动机理论。
华为 Lagrange 数学计算研究中心提出 Sage，一个四阶段分解生成管线加双重信号语义校正循环的自动形式化框架，将答案泄漏率从 70.9% 降至 2.7%，在 Omni-MATH NP 上达到 73.3% pass@4，并在新提出的 IMO-Unformalized 基准上零样本达到 87.4% 验证保真度。
这篇论文提出了一个用于评估数学定理内在趣味性的度量标准，并训练了一个27B模型来预测证明难度，从而能够生成更有趣和新颖的数学成果，同时减少与现有知识库的重叠。
本文介绍了一个框架，使LLMs能够发现和证明有趣的数学定理，通过优化基于证明难度的指标，从而产生更多新颖且有用的数学知识，并减少与现有库的重叠。
本文通过证明与陈述长度之比定义了数学定理的内在趣味性，并训练了一个27B模型来预测证明难度，从而能够生成更有趣的定理，并构建与现有知识（如 Mathlib）重叠更少的自扩展数学知识库。
Mario Carneiro 发现 CIC 加上 LEM 证明了 ZF 集合论的一致性，从而使得在无公理 Lean 中使用 LEM 的证明成为可能，推动了类型论元数学的发展。
文章讨论了人工智能如何革新数学中深刻定理的产生，挑战了传统的成功衡量标准，并以Nivat猜想为重点。