# Abstract — Introduction to Lean: Formalizing Mathematics with Mathlib

*Summer school "Proof assistants and applications", Strasbourg, 31 Aug – 4 Sept 2026.*
*Xavier Roblot (Université Claude Bernard Lyon I).*

> Lean is a proof assistant: a tool in which mathematical statements and their proofs are written in a formal language and checked by the computer. Together with Mathlib, a large library of formalized mathematics developed by its community, it can be used to formalize a wide range of results. This course is an introduction to writing mathematics in Lean and using Mathlib. We will start with the basics — propositions, quantifiers, sets and functions — and then move on to more advanced mathematical territory, such as algebraic structures, analysis and topology, along with the tools available to search the library. No prior experience with formalization is assumed.