Gemini 智能体在 Lean 中生成超 600 万行证明，人工只需审查 1%
Google DeepMind 让 Gemini 智能体写了 600 多万行 Lean 证明，自动审计后人工只看最关键的 1%。做形式化验证或软件安全的人可以看看这套工作流，比纯人工逐行审查省了大量力气。
Google DeepMind 公布 Gemini 智能体在 Lean 形式化证明语言中生成了超过 600 万行数学证明代码，并通过自动审计将人工专家的审查范围压缩到关键部分的 1%。
技术流程上，智能体负责批量生成 Lean 证明，随后系统对代码进行分级审计，自动筛出高风险片段交给人类专家复核。这种分层审校机制解决了形式化验证中证明规模庞大、逐行人工检查成本过高的问题。
该方向指向用 AI 验证关键基础设施的软件与协议正确性，覆盖通信网络到电网等场景。对从事形式化方法、程序验证的团队来说，AI 生成加自动审计的组合可能成为新的大规模验证工作流模板。
Gemini agents generated over 6M lines of proofs in Lean, auditing the code so human experts only had to review the critical 1%. This is a key step toward using AI to verify vital infrastructure we all rely on – from daily communication to power grids. Find out more → goo.gle/4BLrkbk📊 10 ⚡
This report is categorized under AITOP's "Models" desk, focusing on US frontier AI labs and Silicon Valley technology leaders. Within our cross-regional analytical framework, it directly maps to AI developer toolchains, coding agents, and engineering workflows and US-China foundation model benchmarks and commercialization comparison. Key entities and technical topics under continuous tracking include Gemini, DeepMind, Lean, 形式化验证.
Source attribution: curated from Google DeepMind (@GoogleDeepMind).
