标签
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 在代码审计和风格对齐中的实用价值。
Google DeepMind 的新论文介绍了 AlphaProof Nexus，这是一个结合了 LLM 与 Lean 证明检查器的 AI 系统，用于在受限的数学领域中搜索形式化证明。该系统解决了来自 Erdős 和 OEIS 集合的几个未解问题，展示了一种新的分工：AI 提出候选证明，验证器确保正确性。
开发者使用大语言模型和代数重构，在Lean证明助手中正式验证了2023年英国空中交通管制系统崩溃的一个修复补丁，发现LLMs擅长处理证明细节，但在规范说明方面表现不佳。
Vitalik Buterin分享了一个乐观的看法，认为AI辅助的形式化验证是实现安全、无需信任的代码的途径，并链接到他的博客文章，该文章解释了使用Lean进行形式化验证的基础知识。
MathAtlas 是一个针对研究生级别数学的自动形式化的大规模基准测试，包含从103本教科书中提取的约5.2万个定理和定义，并附带一个包含约17.8万条关系的数学依赖图。实验表明，最先进的模型正确率最高仅为9.8%，凸显了其难度。
Signal Shot 是一项重大的形式化验证项目，旨在使用 Lean 验证 Signal 协议及其 Rust 实现。该项目结合了 Rust 到 Lean 的转换（Aeneas）、数学基础（Mathlib/CSLib）、自动化策略（grind/SymM）以及 AI 辅助形式化等方面的最新进展。这是对 Lean 能否从纯数学扩展到已部署的现实世界软件系统的一次重大考验。