标签
LeanFlow是一个LLM智能体系统，用于将数学论文转化为形式化的Lean项目，通过案例研究和与Kimi-K2.6及GPT-5.5的基准测试进行评估，在预算限制内实现了高完成率。
PriorProof 提出了一种方法，通过分析 Lean 证明项相对于更早 Mathlib 快照构建的依赖足迹，来衡量形式化数学中证明技术的新颖性。该方法在 69.7% 的配对上与人类评分者达成一致，并提供可解释的分数差距。
这篇立场论文主张理论级别的自动形式化，即将包括公理、定义和引理在内的整个理论形式化为一致的库，而不是孤立的陈述。它讨论了这种转变的重要性、不同观点、开放挑战，并为形式化研究中的这一转变提出了前进方向。
OpenProver 是一个开源系统，利用 Lean 4 进行 LLM 驱动的自动定理证明，采用规划器-工作器-验证器架构，并支持自主和交互两种模式。它实现了数学证明搜索中的可重复评估和人机协同。
这篇立场论文回顾了LLM驱动的形式化数学的现状，指出了将这些系统应用于开放性研究数学的关键局限性，并提出了一条战略性路线图，用于开发能够推进数学前沿的AI智能体。
Anima Anandkumar 宣布其团队在 ICML 研讨会上发表了四篇与 Lean 相关的论文，涵盖验证机器学习系统、函数式程序合成、证明助手互操作性以及科学推理，将 Lean 定位为 AI 的基础设施。
本文提出了一个用于自然语言到Lean语句忠实形式化的基准测试和评估协议，揭示了编译通过与共识忠实性之间29个百分点的差距，并分解了专家起草、上下文搜索和细化反馈的效果。
Mistral AI 发布了 Leanstral 1.5，这是更新的 Lean 4 形式化证明工程模型，针对自动定理证明和自动形式化进行了优化，总参数为 119B，活跃参数为 6.5B。
本文对五个广泛使用的Lean定理证明基准进行了审计，发现了398个机械可验证的问题，例如反例、空洞定理和不健全的公理。它提出了一个故障分类法、自动化检查器和发布标准，以提高评估的可靠性和可信度。
引入LCS-Bench，这是一个基于计算机科学逻辑的理论级自动形式化基准，覆盖327个教科书条目、4,076个Lean声明。对14个模型的评估表明该基准具有挑战性，最先进模型在自动形式化任务上仅达到20.1%。
本文提出了过程验证强化学习，利用 Lean 证明助手作为过程预言机，在训练期间提供细粒度的策略级反馈，从而提升定理证明性能。
本文介绍了对基于Isabelle构建的自动定理证明工具IsabeLLM的改进，通过集成检索增强生成框架、错误追踪和反例生成。改进后的工具在比特币工作量证明共识协议的形式化验证上进行了评估。
本文提出了一种用于在 Lean 4 中形式化数值分析教材的智能体流水线，并引入了一个超越内核接受的质量审计框架，用于评估语义正确性和库复用情况，揭示了常见的不忠实形式化模式。
本文介绍了一项案例研究，使用大型语言模型（Claude Code）在Lean定理证明器中形式化格罗滕迪克消失定理。研究发现，虽然智能体可以生成经验证的代码，但在定义和API设计方面存在困难，强调了超越单纯编译的专家评审需求。
MA-ProofBench是一个新的形式化基准，用于评估LLMs在数学分析中的定理证明能力，包含200个问题，分为两个难度级别。最佳模型GPT-5.5在Level I上仅达到16%，在Level II上为5%，突显了非形式化推理与形式化推理之间的显著差距。
ATS 是一种静态类型编程语言，它将实现与形式化规范统一起来，支持函数式、命令式、并发和模块化编程，并利用依赖类型和线性类型实现高效和安全。
Gilad Bracha 设想了一个未来，软件工程师使用AI将非正式需求转化为形式化规范并加以审查，而AI则实现代码并用定理证明器验证其是否符合规范。人类负责确保形式化规范正确，他们仅需编写自然语言。
LEAP是一种代理框架，使通用LLMs能够在Lean中实现形式定理证明的最新性能，解决了2025年普特南竞赛的全部12个问题，并在新基准（Lean-IMO-Bench）上将形式化证明率从低于10%提升至70%，超越了专门系统。
提出反馈蒸馏（Feedback Distillation），一种利用来自LLM的token级监督来改进复杂推理的训练方法，在Lean 4定理证明上进行了评估。该方法比GRPO更好地保持了多样性，且两种方法互补。