标签
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 能否从纯数学扩展到已部署的现实世界软件系统的一次重大考验。