A Comprehensive Survey of the Lean 4 Theorem Prover
arxiv.org