人机协作验证数学形式化，防止AI生成内容语义错误。
Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization
- 人机协同确保定义与定理语义正确，避免AI幻觉。
- 自动提取关键节点，大型项目减少94%以上审查量。
- 提出可对齐代码标准，适合数学形式化研究者使用。
AI驱动的数学形式化进展迅速，但证明助手的类型检查仅保证逻辑正确性，无法验证命题和定义是否准确反映其数学意图。因此，AI生成的形式化证明可能通过类型检查却表达错误数学内容。本文提出一种人机协同方法：人类科学家负责语义验证，AI辅助生成。为此开发了Lean Atlas工具，基于Lean 4项目构建交互式依赖图可视化界面，帮助研究人员快速掌握整体结构。核心功能Lean Compass可根据选定定理集，自动提取受其语义影响的关键节点，显著缩小审查范围。在六个不同结构的项目中评估显示：以定理为主的项目（PrimeNumberTheoremAnd、Carleson、Brownian Motion）平均节点减少94%-99%，费马大定理6个定理子集减少59.8%，混合型PhysLib减少69.0%，定义密集型XMSS减少27.3%。提出“对齐形式化代码”作为质量标准，并开源发布于https://github.com/NyxFoundation/lean-atlas。
原文摘要 · Abstract (English)
AI-driven autoformalization of mathematics is advancing rapidly. However, the type checker of a proof assistant guarantees only the logical correctness of proofs; it does not verify whether propositions and definitions faithfully capture their intended mathematical content. Consequently, AI-generated formal proofs can exhibit semantic hallucination-passing the type checker yet failing to express the intended mathematics. We propose a human-in-the-loop approach in which human scientists and AI collaboratively produce formal proofs, with humans responsible for the semantic verification of propositions and definitions. To realize this approach, we develop Lean Atlas, a Lean 4 tool that visualizes the dependency graph of a Lean 4 project as an interactive web viewer, enabling human scientists to grasp the overall structure of a formalization efficiently. Its core feature, Lean Compass, is an algorithm that, given a selected theorem set, automatically extracts the project-specific nodes whose semantic correctness can affect those target statements, thereby reducing the candidate set for semantic review in large-scale formalizations. We further define *aligned Lean code* as formalization code that has undergone human semantic verification, and propose it as a quality standard for AI-generated formalizations. We evaluate the tool on six Lean 4 formalization projects with different structural characteristics; proof-heavy projects (PrimeNumberTheoremAnd, Carleson, Brownian Motion) achieved 94-99% average node reduction, a 6-theorem milestone subset of FLT achieved 59.8%, mixed PhysLib 69.0%, and definition-heavy XMSS 27.3%. Lean Atlas is available as open-source software at https://github.com/NyxFoundation/lean-atlas .
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。