Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization

Researchers Banri Yanahama and Akiyoshi Sannai have introduced Lean Atlas, a new integrated proof environment designed to solve a critical flaw in AI-driven formal mathematics. While AI can rapidly generate proofs that pass a proof assistant's type checker, these proofs can suffer from 'semantic hallucination'—they are logically correct but fail to capture the intended mathematical meaning. Lean Atlas proposes a human-in-the-loop solution where humans verify the semantics of propositions and definitions, while AI handles the heavy lifting of formalization.

At its core is the Lean Compass algorithm, which visualizes a Lean 4 project's dependency graph and, given a target theorem, automatically extracts only the project-specific nodes whose semantic correctness affects it. This drastically reduces the scope of necessary human review. In evaluations on six diverse Lean 4 projects, Lean Compass achieved an average node reduction of 94-99% for proof-heavy projects like the Prime Number Theorem, 69% for mixed projects, and 27.3% for definition-heavy ones. The researchers also define 'aligned Lean code' as a new quality benchmark for AI formalizations that have passed this human semantic verification.

Available as open-source software, Lean Atlas represents a pragmatic framework for scalable collaboration. It doesn't aim to fully automate formalization but to efficiently partition the work: AI generates the formal proof structure at scale, while human experts provide the crucial semantic oversight. This hybrid approach could accelerate the formalization of major mathematical milestones by making the verification process manageable, turning an all-or-nothing task into a scalable, collaborative workflow.