Tag
A reflective essay marking 100 years since Hilbert's program, tracing how Gödel's incompleteness and Turing's halting problem defeated it, and arguing that AI agents powered by proof assistants like Lean now realize Hilbert's 'proof machine' with profound consequences for mathematics and computer science.
A new Meta and NYU paper shows that h1, a simple agent loop giving models fast Lean feedback and search tools, matches or beats hand-designed theorem-proving workflows: it outperformed Goedel-Architect on PutnamBench (598 vs 597 problems) at lower cost, and with Opus 4.8 solved 83/100 hard algebra problems versus 63 for Claude Code.
Podcast interview with Lean creator Leo de Moura on how AI is making formal verification practical, the need to verify AI-generated code and autonomous agents, and the vision of a verified software stack.
This paper introduces RefactorProof, a stress test that derives 458 Lean-certified refactoring variants from VERINA tasks to measure whether LLM-generated proofs remain valid under behavior-preserving program changes. It finds substantial brittleness across reference proofs and specialized provers (DeepSeek-Prover-V2, Goedel-Prover-V2), while noting that most broken proofs can be repaired with small edits.
The paper presents EasyProver, a Lean proving system using recursive agents and asynchronous search that near-saturates PutnamBench and IMO benchmarks with an off-the-shelf frontier model, plus Aegis, a pipeline converting competitive programming into harder real-world Rust-to-Lean verification tasks for benchmarking and RL.
Axiom Math released the first complete computer-checked proof of the Classification of Finite Simple Groups in Lean, using swarms of dozens of AI agents over 24 days to produce ~43.1 million lines of code, while also surfacing 34 deviations from the published record and a new result in group theory.
OpenAI 宣称发布了一篇证明指数时间假设（ETH）为假的论文，主定理已通过 Lean 验证，并由 Impagliazzo、Paturi 和 Williams 领导的独立工作组进行审查；文章通俗解释了 3-SAT、NP 完全性以及 ETH 被证伪可能带来的深远影响。
OpenAI发布了openai/math仓库，包含其未公开内部模型产生的721篇数学手稿（373个结果族），涵盖多个数十年未解问题的突破，并附带约42%结果的Lean形式化证明与模型推理摘要。
本文介绍 PaperFormalizer——一个基于 Lean 的作者参与式自动形式化流程，可从 LaTeX 论文出发构建语句依赖图、审计语句并将其形式化证明，同时在语义存在歧义时让作者做出决策，从而产出经 Lean 验证的论文版本。
作者讲述了自己构建基于Lean的自动定理证明系统的经历，并亲身体验了"苦涩的教训"——模型能力的提升（如GPT-5.6 Sol）远比大量工程优化更能推动进展。
斯坦福研究者通过受控实验研究了在Lean定理证明中，验证器反馈（失败证明与编译诊断）对模型自我修复的影响，发现虽然诊断能改善修复，但自我修复整体上仍无法超越独立重采样。
Google DeepMind and University of Cambridge researchers present a Gemini-based agentic pipeline that autonomously discovers and formally verifies novel Collatz-like accelerations for eleven Busy Beaver BB(6) machines, integrating pattern recognition, automated conjecturing, and Lean theorem proving to advance open-ended mathematical discovery.
Basis researchers used LLMs to write formal semantics for a small programming language and proved in Lean that the interpreter conforms to those rules after compilation to RISC-V, treating the existing interpreter as ground truth to overcome the specification bottleneck in verified software.
A guest post by leading formalization researchers (Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, Adam Topaz) reflecting on AI's rapid theorem-proving advances, cautioning against rushed large-scale formalization efforts like Math, Inc.'s sphere-packing project and Anthropic's Fermat's Last Theorem verification, and outlining a positive vision for high-quality, community-driven formalization of mathematics.
Lean v4.35.0 now ships with multiple verified kernels, including con-leche (the first Lean-written kernel with a formal consistency proof, implemented by Claude) and its Rust-refined counterpart con-ron, plus a new `lake check` command for rechecking developments externally. The move follows AI-discovered kernel soundness bugs and aims to eliminate implementation-level unsoundness without performance penalties.
In a Numberphile interview, Fields Medalist Terence Tao discusses mathematics entering an industrialized era, moving from “proof scarcity” to “proof abundance,” the misalignment of incentives between AI companies and academia, and the risk of human understanding being sidelined.
该论文评估了Lean编译成功是否等同于忠实的自然语言到Lean语句形式化，发现多个系统在编译通过与语义正确之间存在1.3至29.5个百分点的显著差距，且工具增强型代理的大部分差距源于真实的翻译错误。
LeanPRM提出利用Lean证明助手自动为自然语言数学证明生成步骤级正确性标签，无需人工标注即可训练过程奖励模型（PRM）。Qwen3-4B验证器在该数据上训练后，步级标签准确率从48.2提升至74.7，并在IMO级问题的最佳-of-N选择和多个外部验证基准上超越PRM800K训练的验证器。
OpenAI used its AI systems to help produce a formal proof related to the Navier-Stokes equations, but the model mistranslated parts of the mathematics into code during the formalization process.
Thomas Hales writes a guest post for Terence Tao's blog explaining what mathematicians should know about the Lean theorem prover, covering formal proof reliability, the growth of the mathlib library, and how AI-driven autoformalization has become a practical reality in 2026.