标签
提出了一种智能体框架，利用通用编码大语言模型将研究级数学自动形式化为Lean 4代码，并在Putnam问题和STOC会议论文上进行了评估。
本文提出了一个用于自然语言到Lean语句忠实形式化的基准测试和评估协议，揭示了编译通过与共识忠实性之间29个百分点的差距，并分解了专家起草、上下文搜索和细化反馈的效果。
本文对五个广泛使用的Lean定理证明基准进行了审计，发现了398个机械可验证的问题，例如反例、空洞定理和不健全的公理。它提出了一个故障分类法、自动化检查器和发布标准，以提高评估的可靠性和可信度。
本文展示了选择公理在证明空间中存在可测量的几何对应物，利用 Lean 4 的内核级追踪揭示了一个单参数混合律及其对神经定理证明器的操作意义。
本文介绍了一种信号-覆盖矩阵，它将自动形式化中的类型正确性改进分解为四个层级，揭示了LLM改进背后的机制，并表明标题指标可能掩盖实际解决了哪些错误。
该研究提案探讨了不同编程语言中代码库大小如何影响编码LLM的困惑度，并以Lean作为形式语言的测试案例。它表明Lean可能具有更优的缩放指数，从而使大规模软件更安全、更可靠。
引入LCS-Bench，这是一个基于计算机科学逻辑的理论级自动形式化基准，覆盖327个教科书条目、4,076个Lean声明。对14个模型的评估表明该基准具有挑战性，最先进模型在自动形式化任务上仅达到20.1%。
本文介绍了MELD数据集，用于评估文本嵌入模型是否能够捕捉不同术语之间的数学等价性，并发现当前模型无法做到。本文提出了一种对比学习方法，用于对齐非正式和正式的数学表述，从而在非正式-正式检索任务以及自然语言任务上均取得改进。
TheoremGraph 是一个统一的语句级依赖图，涵盖非形式化数学（arXiv 论文）和形式化数学（Lean 项目），利用语义嵌入来弥合两者之间的差距。作者提供了数据集、提取器和 API，以支持数学搜索和检索。
本文提出了过程验证强化学习，利用 Lean 证明助手作为过程预言机，在训练期间提供细粒度的策略级反馈，从而提升定理证明性能。
本文介绍了一项案例研究，使用大型语言模型（Claude Code）在Lean定理证明器中形式化格罗滕迪克消失定理。研究发现，虽然智能体可以生成经验证的代码，但在定义和API设计方面存在困难，强调了超越单纯编译的专家评审需求。
MA-ProofBench是一个新的形式化基准，用于评估LLMs在数学分析中的定理证明能力，包含200个问题，分为两个难度级别。最佳模型GPT-5.5在Level I上仅达到16%，在Level II上为5%，突显了非形式化推理与形式化推理之间的显著差距。
Google新论文提出LEAP框架，将数学问题拆解为目标树，利用Lean验证器反馈进行学习，使LLM在数学竞赛题上的正确率从10%提升至70%，解决了Putnam 2025全部12题，并在IMO基准上超越专用金牌级系统。
谷歌新论文提出LEAP框架，一种智能体框架，使通用大语言模型能够通过规划证明并检查每一步来解决形式化数学问题，在Lean IMO基准测试上将性能从低于10%提升至70%，并解决了所有2025年的Putnam问题。
LEAP是一种代理框架，使通用LLMs能够在Lean中实现形式定理证明的最新性能，解决了2025年普特南竞赛的全部12个问题，并在新基准（Lean-IMO-Bench）上将形式化证明率从低于10%提升至70%，超越了专门系统。
提出反馈蒸馏（Feedback Distillation），一种利用来自LLM的token级监督来改进复杂推理的训练方法，在Lean 4定理证明上进行了评估。该方法比GRPO更好地保持了多样性，且两种方法互补。
Google DeepMind's AlphaProof Nexus 结合了LLM驱动的证明生成与使用Lean的机器验证，解决了353个开放Erdős问题中的9个，其中两个已经开放了56年，每个问题仅花费几百美元。
2026年开年以来，AI以摧枯拉朽的速度完整解决了至少10个Erdős问题，若包括新解则达19个，被视为数学科研的珍妮纺纱机。
陶哲轩演示如何使用 Claude Code 作为红队工具，将 Lean 代码风格对齐 Mathlib 官方风格指南，并以 Riemann–Stieltjes 积分的形式化项目为例，展示了 AI 在代码审计和风格对齐中的实用价值。