标签
Anthropic 的内部 Claude 研究模型于 10 月 16 日独立推翻了指数时间假设（ETH），使用了 1400 万个输出词元，且没有人工输入，相关证明已发布在 GitHub 上。
ReuF2F 引入了一个基于 Lean 4 的基准，包含 244 个源自本科 REU 项目的形式化开放研究问题，用于端到端评估编程智能体。即便是表现最好的模型也只能解决约 40% 的问题，仍有很大的提升空间。
本文介绍了AViD Journal，一个使用Lean 4进行数学定理自动新颖性验证的管道，在撤回的arXiv论文上进行评估，并强调形式验证中的挑战。
这篇立场论文回顾了LLM驱动的形式化数学的现状，指出了将这些系统应用于开放性研究数学的关键局限性，并提出了一条战略性路线图，用于开发能够推进数学前沿的AI智能体。
TheoremGraph 是一个统一的语句级依赖图，涵盖非形式化数学（arXiv 论文）和形式化数学（Lean 项目），利用语义嵌入来弥合两者之间的差距。作者提供了数据集、提取器和 API，以支持数学搜索和检索。
LEAP是一种代理框架，使通用LLMs能够在Lean中实现形式定理证明的最新性能，解决了2025年普特南竞赛的全部12个问题，并在新基准（Lean-IMO-Bench）上将形式化证明率从低于10%提升至70%，超越了专门系统。
Google DeepMind 的新论文介绍了 AlphaProof Nexus，这是一个结合了 LLM 与 Lean 证明检查器的 AI 系统，用于在受限的数学领域中搜索形式化证明。该系统解决了来自 Erdős 和 OEIS 集合的几个未解问题，展示了一种新的分工：AI 提出候选证明，验证器确保正确性。
本文介绍了形式化猜想（Formal Conjectures），这是一个持续演进的基准，包含2615个在 Lean 4 中形式化的数学陈述，其中包括用于证明发现的开放研究猜想和用于自动形式化的已解决问题，旨在零污染地评估自动推理系统。
# 解决（部分）形式化数学奥林匹克问题 来源：[https://openai.com/index/formal-math/](https://openai.com/index/formal-math/) 我们在 [miniF2F](https://arxiv.org/abs/2109.00110) 基准测试上实现了新的最先进成果（41.2% vs 29.3%），这是一个具有挑战性的高中奥林匹克问题集合。我们的方法称为*语句课程学习*，包括手动收集一组难度级别不同的陈述（不含证明）
# 用于自动定理证明的生成语言建模 来源: [https://openai.com/index/generative-language-modeling-for-automated-theorem-proving/](https://openai.com/index/generative-language-modeling-for-automated-theorem-proving/) OpenAI## 摘要 我们探索了基于 Transformer 的语言模型在自动定理证明中的应用。这项工作的动力来自于一种可能性，即自动定理证明器与人类相比的一个主要局限——原始内容的生成