2. Lean Theorem Prover
As mathematics becomes more technical and specialised, rigorously verifying formal proofs is an increasingly costly task. Motivated by the wish to make it easier, recent decades have seen a growing interest in the computational verification of theorems, leading to the development of systems such as Lean, Coq or Isabelle.
Within this field, we distinguish two kinds of formal verification systems: interactive ones (ITPs), which provide an environment where the user guides the proof process step by step, focusing on the "verification" aspect, and automatic ones (ATPs), which aim to complete proofs in a fully autonomous way (Jeremy Avigad et al., 2024)Jeremy Avigad, Leonardo De Moura, Soonho Kong, Sebastian Ullrich, and Lean community contributors, 2024. “Theorem Proving in Lean 4”. Last accessed: April 23, 2025. (Section 1).
In this work we will focus on the use of the Lean Theorem Prover, introduced in 2013 by Leonardo de Moura at Microsoft Research. It is a verifier whose goal is to reduce the distance between assisted and automated proofs, combining a language based on dependent type theory with tools that allow simple sub-problems to be delegated to the system.
Although here we will restrict ourselves to its use as a proof assistant, Lean is also a fully-fledged functional programming language, which offers the user broad possibilities for customisation and automation (Jeremy Avigad et al., 2024)Jeremy Avigad, Leonardo De Moura, Soonho Kong, Sebastian Ullrich, and Lean community contributors, 2024. “Theorem Proving in Lean 4”. Last accessed: April 23, 2025. (Section 1).
In this system, it is possible to define mathematical objects, state properties about them, and prove that those properties hold. This task is made easier by Mathlib, an extensive library of mathematics formalised in Lean, developed collaboratively by an active and constantly growing community (Lean Prover Community)Lean Prover Community. “mathlib4: The Lean4 Mathematical Library”. Last accessed: April 23, 2025..
Proofs are automatically verified by Lean's logical kernel, which guarantees their correctness through an expressive and rigorous type system. Lean's reliability as a proof assistant lies precisely in the simplicity and robustness of this kernel (Christopher A. Bailey and Lean community contributors, 2024)Christopher A. Bailey and Lean community contributors, 2024. “Type Checking in Lean 4”. Last accessed: April 23, 2025..
In this section we will mainly follow the online manual Theorem Proving in Lean 4 (Jeremy Avigad et al., 2024)Jeremy Avigad, Leonardo De Moura, Soonho Kong, Sebastian Ullrich, and Lean community contributors, 2024. “Theorem Proving in Lean 4”. Last accessed: April 23, 2025., which is an updated version of the book Theorem Proving in Lean (Jeremy Avigad, Leonardo De Moura, and Soonho Kong, 2021)Jeremy Avigad, Leonardo De Moura, and Soonho Kong, 2021. “Theorem proving in Lean”. , published in 2021, adapted to the new version of Lean. At the theoretical level there is no great difference between the two, so both references are valid for understanding the foundations we present here.