An Introduction to Lean 4

An Introduction to Formal Verification

Autor

Enric Cosme

Modificat

02/04/2025

Introduction

Lean 4 is a versatile programming language and interactive theorem prover designed to formalize mathematics, verify software, and explore computational logic. Whether you are a mathematician, computer scientist, or a curious learner, Lean 4 offers powerful tools for rigorous reasoning and proof verification. By combining programming and formal reasoning, Lean 4 serves as an essential tool for both learning and research.

Lean 4 enables us to:

  • Prove Theorems: Formalize and verify mathematical proofs with precision, eliminating ambiguities and errors.
  • Write Programs: Develop functional programs with strong type safety and reliability.
  • Verify Systems: Ensure the correctness of software and hardware through formal verification techniques.
  • Explore Logic: Study dependent type theory, proof automation, and formal methods in depth.

This manual introduces the fundamentals of Lean 4, covering Basic syntax and types, Theorem proving and verification, and Practical applications in mathematics and computer science. Each chapter includes examples, exercises, and practical insights to help us build confidence and proficiency in Lean 4. The content of this manual is based on informal seminar sessions conducted by the author at the Universitat de València and taught to master’s students at Nantong University. These sessions focus on foundational topics in mathematics, particularly the universal properties of key constructions.

A Brief History of Lean

Lean was developed by Leonardo de Moura and his team at Microsoft Research in 2013. It was created to provide a robust and scalable framework for formalizing mathematics, verifying software, and exploring type theory.

Over the years, Lean has evolved significantly, with Lean 4 offering improved performance, a redesigned type system, and enhanced support for metaprogramming. Today, it serves as a foundational tool for both theoretical and applied research in mathematics and computer science.

To learn more about Lean 4, visit the official website: lean-lang.org.

References and Learning Resources

While this manual provides a thorough introduction to Lean 4, there are many other excellent resources available to deepen your understanding. Here are some recommended materials:

  1. Functional Programming in Lean: The standard reference for learning how to use Lean as a programming language.
  2. Theorem Proving in Lean 4: A comprehensive guide to using Lean as a theorem prover.
  3. Mathematics in Lean: A resource focused on using Lean for formalizing mathematics.
  4. The Mechanics of Proof: Lecture notes designed for early university-level students on writing rigorous mathematical proofs.
  5. Lean Language Reference: A technical document describing the syntax, semantics, and standard library of Lean.
  6. Documentation Overview: A collection of examples, developer guides, and other essential documentation.
  7. Lean Community Learning Resources: A curated list of tutorials, guides, and documentation sources for Lean 4.
  8. Lean Zulip Chat: Join the public chat room to engage with the Lean community and seek guidance.

Installation and Quickstart Guide

To start using Lean 4, follow the Quickstart Guide from the official documentation. This guide provides step-by-step instructions on installing Lean 4 on our system, setting up a development environment and writing and running our first Lean program

For the best experience, it is recommended to use Lean 4 with VS Code and the Lean extension, which provides syntax highlighting, interactive proof support, and an enhanced development workflow.

With these foundational insights, we are now ready to dive into Lean 4 and explore its capabilities in programming, formal verification, and theorem proving. Let’s get started!

Acknowledgements

Writing this textbook has been a personal endeavor, but it would not have been possible without the support and encouragement of many individuals and institutions.

First and foremost, I would like to express my deepest gratitude to the Universitat de València and Nantong University for providing an environment conducive to research and teaching, which greatly influenced the development of this book.

I am deeply grateful to my students, both past and present, whose curiosity and thoughtful questions have continually inspired me to refine my explanations and enhance the clarity of the material presented here. In particular, I would like to express my heartfelt appreciation to Yan Yan for her keen insight and enthusiasm, which have been a driving force behind this project.

I would also like to acknowledge the contributions of the broader academic and open-source communities, especially the developers and maintainers of Lean and Quarto, whose work has enabled the seamless integration of formal verification and programming into this text.

Finally, to all who have contributed in ways large and small, whether through direct collaboration or simply by offering words of motivation—thank you.