This talk will present an overview of our lab's research at the intersection of artificial intelligence and formal mathematics using the Lean theorem prover. I will discuss our foundational projects including LeanDojo, Lean Copilot, and LeanAgent, which collectively establish a framework for making formal verification more accessible to working mathematicians through AI assistance. Beyond these core systems, I will highlight several specialized applications, including our work on autoformalization of Euclidean geometry, proof progress prediction, and emerging efforts to apply Lean verification to scientific domains. Our broader goal is to extend the power of formal verification beyond pure mathematics into AI4Science applications, such as verifying solutions to partial differential equations and ensuring correctness in scientific computing. By bridging traditional mathematical practice with formal verification through AI assistance, our work aims to enhance both the accessibility and reliability of mathematical reasoning across disciplines.