标签
该论文确定了在独立非同分布噪声和两两非负相关噪声下，选择最大噪声分数所产生的“赢家偏差”的尖锐常数界，并将全部定理在 Lean 4 中形式化验证，同时在 448 个模型选择流程上验证了结论的实际意义。
一篇论文展示了简单智能体框架（h1）配合高效的 Lean 4 反馈接口，在 PutnamBench、FATE-X 和 FormalConjectures 上达到了最先进的形式定理证明结果，不逊于甚至超越了专门设计的多步工作流，并解决了八个公开问题。作者认为执行接口比复杂的编排更为重要，并警告在未用高效反馈评测前沿模型之前，不要过早规定结构化工作流。
普渡大学的一篇论文提出了一种有界的在线步骤级修复模块，用于 Lean 4 定理证明器。该模块将编译器错误信息输入预训练的修复模型，而不是直接丢弃失败的策略，在 LeanDojo 基准测试上求解率相对提升最高达 32%，并在 Lean Workbook 上性能几乎翻倍。
开发者用 Lean 4 完整实现了 RealWorld（Medium 克隆）参考应用，前后端全部使用 Lean 编写，并借助社区库（HTTP 服务器、Postgres 驱动、JWT、HTML 渲染等）通过官方 API 与网站测试套件。文章以数学论文风格呈现，部分关键性质以定理形式在 Lean 中形式化验证。
作者们提出 Choir——一个用于分布式多智能体自动形式化的开放、模块化协议，将项目拆解为基于 GitHub 的任务，并通过确定性的信任门验证机制进行审核，支持 Lean 4、Isabelle 和 Rocq；该项目包含一篇预印本以及一个由 DARPA expMath 项目资助的开源代码仓库。
该论文提出了 LeanPolish，这是一个符号化的 Lean 4 流水线，发布了超过 33k 条可验证的证明修改记录及失败尝试。研究表明，可验证监督数据可能存在搜索过程引入的伪影，而对符号化压缩步骤进行迭代改进，在 miniF2F 上优于神经混合方法，并在 PutnamBench 上适度提升了整体证明重写效果。
华为 Lagrange 数学计算研究中心提出 Sage，一个四阶段分解生成管线加双重信号语义校正循环的自动形式化框架，将答案泄漏率从 70.9% 降至 2.7%，在 Omni-MATH NP 上达到 73.3% pass@4，并在新提出的 IMO-Unformalized 基准上零样本达到 87.4% 验证保真度。
OpenAI宣布使用Lean 4为Navier-Stokes方程提供了形式化证明，将形式化验证的成本从数万小时减少到仅17小时，突显了人工智能在数学和验证中的变革性作用。
StochBench 引入了一个包含 450 个研究生水平随机过程问题的领域特定基准测试，使用 Lean 4 实现，并通过一个 AI 代理评估，证明率达到 34.9%，以推进应用数学中的形式化定理证明。
本文介绍了AViD Journal，一个使用Lean 4进行数学定理自动新颖性验证的管道，在撤回的arXiv论文上进行评估，并强调形式验证中的挑战。
MathCode是一款AI驱动的编码助手，它能将数学问题转换为Lean 4定理并尝试进行形式化证明，具有持久化的REPL、定理库以及代理模式证明功能。
一篇研究论文，介绍了一种故障触发级联方法，用于将机器学习安全地集成到Lean 4的grind策略中，实现了效率提升并解决了之前无法解决的证明，且没有回归问题。
本文介绍了FVSpec，这是一个用于AI辅助形式验证的基准测试，它通过多智能体LLM管道将真实世界的基于属性测试从Python转换为Lean 4规范，旨在推动真实世界软件形式验证的进展。
Aleph Prover 已在 Lean 4 中形式化了 OpenAI 对保罗·埃尔德什平面单位问题的反证，并将其作为开源发布以供独立验证，展示了人工智能在加速数学研究中的作用，同时提供了可验证的证明数据。
本文在Clever基准的程序验证任务中，采用智能体证明框架评估Claude Code，在规范生成和端到端验证方面取得了超过98%的成功率，揭示出现有基准可能不足以评估现代智能体证明器的能力。
OProver是一个统一的框架，用于Lean 4中的代理式形式定理证明，通过使用经过验证的证明和编译器反馈进行训练，迭代地改进证明生成，在多个基准测试中取得了最先进的结果。
TorchLean 是一款全新发布的 Lean 4 框架，可实现神经网络软件的形式化验证，具备类型化张量、可验证自动微分、PyTorch 互操作性及 GPU 执行等特性。此次发布进一步扩展了对扩散模型、GPT 风格 Transformer 和状态空间模型等现代架构的支持，将实际的机器学习工作流与数学证明检查紧密连接。
本文介绍了 Discover and Prove (DAP)，一个用于 Lean 4 自动定理证明的开源智能体框架，针对"困难模式"问题进行优化——即在构造形式化证明前必须独立发现答案。该工作发布了新的困难模式基准变体，达到最先进的结果，同时揭示了 LLM 答案准确率（>80%）与形式化证明器成功率（<10%）之间的巨大差距。