Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization — Banri Yanahama, Akiyoshi Sannai | Kutubxona