Lean is an interactive theorem prover that is revolutionizing how mathematical proofs are written and verified. As an open-source project, Lean has fostered a growing community of mathematicians, logicians, and programmers who are collaboratively building a comprehensive library of formalized mathematics. This talk will introduce Lean’s core concepts, explore its underlying type theory, and demonstrate how it enables rigorous, computer-verified proofs. No prior experience with proof assistants is required.