标签
介绍了FaithformBench，一个用于评估数学思维链自动形式化系统忠实度的基准，通过测量扰动步骤上的有效性与无效性保持来评估。应用于八个AF系统后，揭示了普遍的“谄媚”现象，即无效输入被静默纠正。
与 Lean 和 Z3 的创造者 Leonardo de Moura 的访谈节目，讨论 Lean 的工作原理、LLM 在形式化验证中的作用，以及 AI 辅助证明如何改变软件开发和数学。
OpenAI 未发布的模型 Astra 据称解决了十大开放数学难题，结果已通过 Lean 证书形式化验证，标志着 AI 数学推理能力的重大飞跃。
OpenAI 报告称，其下一代主要模型的内部版本（Astra）以约2000美元的token成本，解决了数学和理论计算机科学领域10个长期悬而未决的开放问题，并附有正式的Lean证书。
本文介绍了一种三阶段LLM流水线，用于系统性地生成和验证重大数学猜想，利用Lean 4形式化验证和反思性验证来发现具有高“问题品味”的问题。
对 Lean 内核中一个可靠性漏洞的事后剖析，该漏洞被利用来产生考拉兹猜想的“反证”，并说明了修复方案以及为什么独立的检查器最初也未能发现它。
Lawrence Paulson 讨论了因 Lean 内核中的一个 bug 导致的 Collatz 猜想的虚假反驳，并对证明对象和证明助手的可靠性进行了思考。
一个由AI生成的Lean形式化证明声称推翻了Collatz猜想，实际上利用了Lean内核中的两个漏洞（现已修复）。Lean创始人Leo de Moura警告说，这种情况还会继续发生，因为AI非常擅长发现健全性漏洞。
一篇技术博文认为，由于Rocq（Coq）原生支持余归纳类型和cofixpoints，而Lean基于库的方法尚不成熟，因此Rocq在程序验证方面优于Lean。
本文讨论了LLMs如何自动生成证明，在如Lean和Rocq这样的依赖类型语言中，通过利用证明无关性并减少手动证明工程的需求，使得形式验证变得更加实用。
LeanFlow是一个LLM智能体系统，用于将数学论文转化为形式化的Lean项目，通过案例研究和与Kimi-K2.6及GPT-5.5的基准测试进行评估，在预算限制内实现了高完成率。
一个经 Lean 验证的新形式定理表明，对于趋向无穷的阈值，几乎所有正整数都在 436 ln N 个 Collatz 步内降至该阈值以下，强化了陶哲轩先前的结果，并给出了显式界限和自然密度。
PriorProof 提出了一种方法，通过分析 Lean 证明项相对于更早 Mathlib 快照构建的依赖足迹，来衡量形式化数学中证明技术的新颖性。该方法在 69.7% 的配对上与人类评分者达成一致，并提供可解释的分数差距。
包括ChatGPT和OpenAI的Sol在内的人工智能系统，已经驳斥并完全形式化了Erdős单位距离猜想，标志着人工智能辅助数学的一个里程碑。文章讨论了这一过程及其对数学证明验证未来的影响。
研究人员使用20个并行Codex账户解决了20个Erdős问题，其中包括使用Lean对数论中的Erdős问题#123的形式化证明。
微软研究院提出了一种新方法，使用Rust、Lean、Aeneas和AI代理来形式化验证密码学代码，实现了对ML-KEM和SHA-3等生产算法的可扩展验证，同时保持性能。
马特·帕克的视频探讨了近期AI（包括ChatGPT）帮助解决未解的Erdős问题的案例，彰显了AI辅助数学发现的新时代。
Anima Anandkumar 宣布其团队在 ICML 研讨会上发表了四篇与 Lean 相关的论文，涵盖验证机器学习系统、函数式程序合成、证明助手互操作性以及科学推理，将 Lean 定位为 AI 的基础设施。
LeanstralSafeVerify 是一个安全验证工具，用于确保 Lean 代码符合规范，防范漏洞攻击，已应用于多个 Web 应用和排行榜。