This is an invitation to explore Lean 4, a modern programming language and interactive theorem prover. Lean is not only a tool for writing reliable software, but also a framework for developing rigorous, computer-verified mathematics. Its unique combination of programming and formal reasoning makes it a powerful resource for students, researchers, and practitioners who wish to bridge the gap between mathematics and computer science.

The main goal of this text is to provide a clear and gradual introduction to Lean 4, starting from the fundamentals of programming–syntax, types, functions, and data structures–and moving towards the core principles of formal proof, such as propositions, quantifiers, equality, and inductive reasoning. Along the way, we will study essential mathematical constructions including relations, subtypes, quotients, and orders, emphasizing their universal properties and their role in formalization. Each chapter combines exposition, examples, and exercises, carefully designed to help readers build both intuition and technical fluency. Exercises range from straightforward practice problems to more challenging tasks that encourage deeper exploration. This manual is available both as a web version and as a PDF. All exercises in this manual are accompanied by solutions available on GitHub, making the material suitable for self-study as well as classroom use.

The material presented here has grown out of seminar sessions at the Universitat de València and courses for master’s students at Nantong University. Our guiding principle has been to present Lean not as an abstract system, but as a living environment where mathematical ideas can be expressed, tested, and verified.

By the end of this book, readers will not only know how to write Lean 4 programs and construct formal proofs, but also appreciate the broader significance of formal verification: ensuring correctness, reducing ambiguity, and deepening our understanding of mathematics itself.