Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization. - Banri Yanahama; Akiyoshi Sannai (CoRR, 2026)