Mathematical formalization has attracted increasing attention in recent years, with Lean 4 emerging as one of the central tools in this area. This series of four seminars will introduce mathematical formalization, discuss its significance, and showcase recent examples of successful formalization projects. Two of the seminars will provide hands-on tutorials using the interactive theorem prover Lean 4. In the final seminar, we will examine how artificial intelligence and formalization interact, highlighting recent developments in autoformalization and automatic theorem proving.