标签
普渡大学的一篇论文提出了一种有界的在线步骤级修复模块，用于 Lean 4 定理证明器。该模块将编译器错误信息输入预训练的修复模型，而不是直接丢弃失败的策略，在 LeanDojo 基准测试上求解率相对提升最高达 32%，并在 Lean Workbook 上性能几乎翻倍。
# 数学家们对 OpenAI 重大发现的百条短评 100 多位数学家对 OpenAI 于 10 月 6 日发布的公告做出了简短回应。OpenAI 宣布其模型已解决了 100 多个悬而未决的数学难题，其中包括对"准黎曼猜想"等突破性成果的震惊，以及对人类数学家未来角色的深刻反思。
UT Austin 数学系主任 Francesco Maggi 表示，OpenAI 似乎正准备一次性发布约 400 份 AI 生成的数学证明，这表明数学发现可能不再是什么稀缺资源——真正稀缺的将是人类的理解力。
本文介绍了一种在Lean中利用LLMs自动生成具有完备性形式化证明的泛化规划的方法，并在基准领域上进行了评估，展示了在自动规划验证方面的显著进步。
Verus 是一个开源的自动化程序验证器，专为 Rust 设计，通过数学证明帮助确保代码正确性，并被亚马逊用于像 Nitro Isolation Engine 这样的项目。
ProofEvolve是一个神经符号框架，通过使用神经模型进化形式化验证的证明结构来增强自动定理证明，通过保留来自未完成尝试的验证知识，在Lean基准测试中实现高求解率。
该论文介绍了FAR，一种人机发现范式，它自动化了从文献中搜索数学问题的过程，并在组合数学的试点中展示了其在识别猜想和解决方案方面的有效性。
一个名为 Theo Conjecture 的AI系统，利用了大型语言模型，解决了一个35年前的图论问题，该问题最初由数学家 Paul Erdős 提出，发现了一个意想不到的项。该系统通过循环提出、测试和修正数学想法来工作。
一篇研究论文，介绍了一种故障触发级联方法，用于将机器学习安全地集成到Lean 4的grind策略中，实现了效率提升并解决了之前无法解决的证明，且没有回归问题。
OpenProver 是一个开源系统，利用 Lean 4 进行 LLM 驱动的自动定理证明，采用规划器-工作器-验证器架构，并支持自主和交互两种模式。它实现了数学证明搜索中的可重复评估和人机协同。
Research Math Agents (RMA) 是一个用于研究级数学问题自动推理的智能体框架，在 First Proof 基准测试中取得最先进结果，解决了10个问题中的8个，优于 GPT-5.2R 和 Aletheia 等强基线。
本文介绍了形式化猜想（Formal Conjectures），这是一个持续演进的基准，包含2615个在 Lean 4 中形式化的数学陈述，其中包括用于证明发现的开放研究猜想和用于自动形式化的已解决问题，旨在零污染地评估自动推理系统。