Welcome

What is the goal of this week?

• You will learn how to use Lean, an interactive theorem prover, and its mathematical library mathlib.

• Every day there will be tutorials explaining the basics, but also exercise sessions where you can practice what you have learnt.

• There will also be more advanced talks, to give an idea of what current research on formalized mathematics looks like.

Before we start

Please follow the installation instructions at

https://github.com/riccardobrasca/LFTCM2026/

If you had trouble following the instructions, no worries for this talk: you can just follow along, and ask for help right afterwards.

What is formalization?

Formalization means using a computer to reason.

More concretely, it means writing mathematics in a language precise enough that a computer can check every single step of an argument.

• Nothing may hide behind “obvious” or “similarly”: the result is unambiguous and machine-checkable.

• Along the way we often gain a better understanding of the mathematics itself.

• Modern formalization is done with proof assistants, which provide notation, automation, and immediate feedback.

Lean and mathlib

• Lean is open source, and is both a functional programming language and a proof assistant. Leonardo de Moura started it in 2013; Lean 4 is the current version.

• Rocq, Isabelle and Agda are other major proof assistants, but Lean has become the one of choice for many research mathematicians.

• mathlib is Lean's community-maintained mathematical library, written by hundreds of contributors.

• Overall it is at the level of a graduate student in mathematics, and it also contains some research-level results.

• Everything lives in one coherent library, so all results are stated in compatible terms and can be combined freely.

The elephant in the room

• I've heard that AI is extremely good at autoformalization. What is the point, then?

• Yes, this is true, but the same holds for linear algebra, and you probably still teach it. Autoformalization is useful to check correctness, for example of AI-generated proofs, but this is not the only goal of formalization.

• Besides, formalization is an interesting and genuinely enjoyable scientific activity in its own right.

• Definitions and statements still need to be checked by humans.

More on this subject on Wednesday afternoon.

What we propose for the week

• In the repository there is a file Exercises.md, with various mathematical statements in plain English, each with an indication of its difficulty.

• Pick a couple of them, and try to formalize both the statement and a proof.

• These are two rather different tasks: formalizing the statement is of course easier, unless the proof is already in mathlib.

• You are of course free to work on something else. Just check with one of us that it is a reasonable target.

The goal is to have this done by the end of the week.

Let's start

Let's start playing with Lean!