标签
本文介绍了一种在Lean中利用LLMs自动生成具有完备性形式化证明的泛化规划的方法，并在基准领域上进行了评估，展示了在自动规划验证方面的显著进步。
这条推文讨论了使用形式验证方法如 TLA+ 和 Lean 来确保关键任务 AI 基础架构软件的正确性和可扩展性，并提到了 Intent Lab 和 Boris Cherny 在 Claude Agent SDK 方面的工作。
作者使用 Claude 的 Opus 5.5 模型通过 Lean 对 Claude Agent SDK 进行了形式化验证，生成了 16 个 PR 来修复 bug 和竞态条件，并建议结合 Lean 和 TLA+ 以增强 bug 查找能力。
Mario Carneiro 发现 CIC 加上 LEM 证明了 ZF 集合论的一致性，从而使得在无公理 Lean 中使用 LEM 的证明成为可能，推动了类型论元数学的发展。
本文探讨了OpenAI针对Navier-Stokes问题的Lean证明的验证，强调了确保形式证明与预期数学问题一致的重要性，以及数学家进一步审查的必要性。
OpenAI声称发现了一个由AI生成的纳维-斯托克斯方程解，这是一个有200年历史的数学问题，但学术界人士正在争议其归属，并指责OpenAI在得知他们的工作后仓促行事。
OpenAI 在 GitHub 上发布了新的 Lean 定理证明仓库，这是在其即将发布的 Astra 之前。
本文介绍了SA-Pass，一种用于评估自动形式化中语义对齐的方法，并提出了ShadowBench，一个包含178个问题的Lean 4基准测试，展示了与专家判断的高度一致性。
Levent Alpöge声称用Claude撰写了一个100页的Hopf问题证明，而OpenAI的Boris Alexeev在短短几天内使用Codex将其形式化为250,000行Lean代码。
FormalTCS是一个用于评估大型语言模型在端到端理论计算机科学研究上的基准，揭示了显著局限性，尤其是在自动形式化方面。
这篇文章反映了前沿大语言模型和Lean自动化如何大幅减少了编程语言研究中形式化证明所需的工作量，导致会议投稿数量翻倍并改变了出版规范。
介绍了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非常擅长发现健全性漏洞。