Lean Atlas 把 AI 形式化的“语义忠实性”提升为独立审计层，而不再只看 typecheck

Lean Atlas 针对 AI-generated Lean code 的 semantic hallucination 问题：proof assistant 能保证逻辑上 type-correct，却不能保证 formal proposition 真正表达原始数学含义。系统用 dependency-graph visualization 与 Lean Compass 自动提取会影响目标 theorem 的 project-specific semantic nodes，让人类只审核关键 definitions / propositions。论文在多个项目上报告 proof-heavy developments 可减少约 94%–99% 的人工语义审查候选节点，并提出 aligned Lean code 作为质量标准。