\chapter{Preface}

Formal proof assistants are pieces of software designed to help their users
carry out computer-checked proofs. We usually call them
\emph{proof assistants}, or \emph{interactive theorem provers}, but a
frustrated student coined the phrase ``proof-preventing beasts,'' and dictation
software occasionally misunderstands ``theorem prover'' as ``fear improver.''
Consider yourself warned.

\paragraph{Rigorous and Formal Proofs}

Interactive theorem proving has its own terminology, starting with the
notion of ``proof.'' A \emph{formal proof} is a logical argument expressed
in a logical formalism. In this context, ``formal'' means ``logical'' or
``logic-based.'' Logicians---the mathematicians of logics---carried out formal
proofs on paper decades before the advent of computers, but nowadays formal
proofs are almost always carried out using a proof assistant.

In contrast, an \emph{informal proof} is what a mathematician would normally
call a proof. These are often carried out in \LaTeX{} or on a blackboard,
and are also called ``pen-and-paper proofs.'' The level of detail can vary a
lot, and phrases such as ``it is obvious that,'' ``clearly,'' and ``without
loss of generality'' move some of the proof burden onto the reader. A
\emph{rigorous proof} is a very detailed informal proof.

The main strength of proof assistants is that they help develop highly
trustworthy, unambiguous proofs of mathematical statements, using a precise
logic. They can be used to prove arbitrarily advanced results, going well
beyond toy examples and logic puzzles. Formal proofs also help students
understand what constitutes a valid definition or a valid proof. To quote
Scott Aaronson:%
\footnote{\url{https://www.scottaaronson.com/teaching.pdf}}
%
\begin{quote}
I still remember having to grade hundreds of exams where the students started
out by assuming what had to be proved, or filled page after page with
gibberish in the hope that, somewhere in the mess, they \emph{might}
accidentally have said something correct.
\end{quote}

When we develop a new theory, formal proofs can help us explore it. They are
useful when we generalize, refactor, or otherwise modify an existing proof, in
much the same way as a compiler helps us develop correct programs. They offer a
high level of trustworthiness, making it easier for others to review them. In
addition, formal proofs can form the basis of verified computational tools
(e.g., verified computer algebra systems).

\paragraph{Success Stories}

There have been a number of proof assistant success stories in mathematics and
computer science. Some landmark results in the formalization of mathematics
have been the proof of the four-color theorem by Gonthier et
al.~\cite{gonthier-2008}, the proof of the odd-order theorem by Gonthier et
al.~\cite{gonthier-et-al-2013}, the proof of the Kepler conjecture by Hales
et al.~\cite{hales-et-al-2015}, and the definition of perfectoid spaces by
Buzzard et al.~\cite{buzzard-et-al-2020}. The earliest work in this area was
carried out by Nicolaas de Bruijn and his colleagues starting in the 1960s in a
system called AUTOMATH.%
\footnote{\url{https://www.win.tue.nl/automath/}}

A few companies, including AMD \cite{russinoff-1999} and Intel
\cite{harrison-2003}, have been using proof assistants to verify their designs.
In academia, some of the milestones are the verifications of the operating
system kernels seL4 \cite{klein-et-al-2010} and CertiKOS \cite{gu-et-al-2016}
and the development of the verified compilers CompCert \cite{leroy-2009-jar},
JinjaThreads \cite{lochbihler-2010}, and CakeML~\cite{kumar-et-al-2014}.

\paragraph{Proof Assistants}

There are dozens of proof assistants in development or use across the world. A
list of the main ones follows, grouped by their logical foundation:

\begin{itemize}
\item set theory: Isabelle/ZF, Metamath, Mizar;
\item simple type theory: HOL4, HOL Light, Isa\-belle\slash HOL;
\item dependent type theory: Agda, Coq, Lean, Matita, PVS;
\item Lisp-like first-order logic: ACL2.
\end{itemize}

For a history of proof assistants and interactive theorem proving, we refer to
Harrison, Urban, and Wiedijk's highly informative chapter
\cite{harrison-et-al-2014}.

\paragraph{Lean}

Lean is a proof assistant developed primarily by Leo\-nardo de Moura (Microsoft
Research) since 2012. Its mathematical library, \li{mathlib}, was originally
developed under the leadership of Jeremy Avigad (Carnegie Mellon University) but
is now maintained and further extended by the user community
\cite{mathlib-mathlib-2020}.%
\footnote{\url{https://github.com/leanprover-community/mathlib4}}

This guide uses Lean version \leanversion,
\li{mathlib} revision \mathlibrevision, and a few extensions collected in a
small library called \li{LoVelib}.%
\footnote{
\ifdefined\LMU
  \url{https://github.com/blanchette/interactive_theorem_proving_2024/raw/main/lean/LoVe/LoVelib.lean}
\else
  \url{https://github.com/lean-forward/logical_verification_2024/raw/main/lean/LoVe/LoVelib.lean}
\fi}
Although it is a research project, with some rough edges, there are several
reasons why Lean is suitable to teach interactive theorem proving:

\begin{itemize}
\item It has a highly expressive, and very interesting, logic based on the
    calculus of inductive constructions, a dependent type theory.

\item It is extended with classical axioms and quotient types, making it
  useful to verify mathematics.

\item It includes a convenient metaprogramming framework, which can be used
  to program custom proof automation.

\item It includes a modern user interface via a Visual Studio Code plugin.

\item It has highly readable, fairly complete documentation.

\item It is open source.
\end{itemize}

Lean's core library includes only basic algebraic definitions. More
definitions are found in \li{mathlib}. Despite its name, \li{mathlib} is more
than a mathematical library; it provides a lot of basic automation on top of
Lean's core library, as one would expect from a modern proof assistant.

\paragraph{This Guide}

This guide was originally designed as a companion to the MSc-level course
Logical Verification (LoVe) taught at the Vrije Universiteit Amsterdam. Its
primary aim is to teach interactive theorem proving. Lean is the means, not an
end in itself. As such, this guide is not designed to be a comprehensive Lean
tutorial---for this, we recommend \emph{Theorem Proving in Lean 4}
\cite{theorem-proving-in-lean}. This guide is also no substitute for doing the
exercises and homework. Theorem proving is not for spectators; it can only be
learned by doing.

Specifically, the aim is that you
%
\begin{itemize}
\item learn the fundamental theory and techniques of interactive theorem
  proving;

\item learn how to use logic as a precise language for modeling systems and
  stating properties about them;

\item become familiar with some areas in which proof assistants are
  successfully applied, such as functional programming, the semantics of
  imperative programming languages, and mathematics;

\item develop practical skills that can be applyed in larger projects (whether
  personal or for an MSc or PhD or in industry);

\item feel able to move to another proof assistant and
  apply what you have learned;

\item get to understand the domain well enough to start reading relevant
  scientific papers published at international conferences such as Certified
  Programs and Proofs (CPP) and Interactive Theorem Proving (ITP) or in journals
  such as the \emph{Journal of Automated Reasoning} (JAR).
\end{itemize}

Equipped with a good knowledge of Lean, it should be easy to move to
another proof assistant based on dependent type theory, such as Agda or Coq, or
to a system based on simple type theory, such as HOL4 or Isa\-belle\slash HOL.

An important characteristic of this guide, which it shares with Knuth's
\emph{\TeX{}book} \cite{knuth-1986}, is that it does not always tell the truth.
To simplify the exposition, some basic but false claims are made about Lean.
Most of these statements are then rectified in later chapters. Like Knuth, we
feel that ``this technique of deliberate lying will actually make it easier for
you to learn the ideas. Once you understand a simple but false rule, it will
not be hard to supplement that rule with its exceptions.''

The Lean files accompanying this guide can be found in a public repository.%
\footnote{
\ifdefined\LMU
  \url{https://github.com/blanchette/interactive_theorem_proving_2024}
\else
  \url{https://github.com/lean-forward/logical_verification_2024}
\fi}
The files' naming scheme follows this guide's chapters; thus,
\verb|LoVe07_|\allowbreak\verb|Effectful|\-\verb|Programming_|\allowbreak\verb|Demo.|\allowbreak\verb|lean|
is the main file associated with Chapter~\ref{chap:effectful-programming} (``Effectful Programming''), reviewed
in class,
\verb|LoVe07_|\allowbreak\verb|EffectfulProgramming_|\allowbreak\verb|Exercise|\-\verb|Sheet.|\allowbreak\verb|lean|
is the exercise sheet, and
\verb|LoVe07_|\allowbreak\verb|EffectfulProgramming_|\allowbreak\verb|Homework|\-\verb|Sheet.|\allowbreak\verb|lean|
is the homework sheet.

We owe a huge debt to the authors of \emph{Theorem Proving in Lean 4}
\cite{theorem-proving-in-lean} and \emph{Concrete Semantics:\ With
Isabelle\slash HOL}~\cite{nipkow-klein-2014}, who have taught us Lean and
programming language semantics. Many of their ideas appear in this guide.

We thank Robert Lewis and Assia Mahboubi for their useful comments on this
guide's organization and focus. We thank Kiran Gopinathan and Ilya Sergey for
sharing the anecdote reported in footnote \ref{foot:false-anecdote} of
Chapter~\ref{chap:programs-and-theorems} and letting us share it further. We
thank Daniel Fabian for designing the first tablet-optimized version of this
guide. We thank Paul Chisholm for authoring some of the comments in the
associated Lean files. We thank Mark Summerfield for his many textual
suggestions. Finally, we thank Chris Bailey, Kevin Buzzard, Paul
Chisholm, Dominique Danco, Raufs Dunamalijevs, Wan Fok\-kink, Lina Gerlach,
Robert Lewis, Pietro Monticone, Antonius Danny Reyes, Robert Sch\"utz, Patrick
Thomas, Balazs Toth, Huub Vromen, Floris Westerman, and Wijnand van Woerkom for
reporting typos and some more serious errors they found in earlier editions of
this guide. Should \emph{you} find some mistakes in this text, please let us
know.%
\footnote{\href{mailto:jasmin.blanchette@ifi.lmu.de}{\texttt{jasmin.blanchette@ifi.lmu.de}}}

\paragraph{Special Symbols}

In this guide, we assume that you will be using Visual Studio Code and its
``lean4'' extension to edit \verb|.lean| files. Visual Studio Code lets you
enter Unicode symbols by entering backslash \li{\} followed by an ASCII
identifier. For example, \li{→}, \li{∀}, or \li{∈} can be entered by typing
\li{\->}, \li{\fo}, or \li{\in} and pressing the tab key or the space bar. We
will freely use these notations. For reference, we provide a list of the main
non-ASCII symbols that are used in this guide and, for each, one of its ASCII
representations. By hovering over a symbol in Visual Studio Code while holding
the control or command key pressed, you will see the different ways in which it
can be entered.

\vskip3\smallskipamount

\begin{center}
\tabletsmall
\begin{tabular}{@{}l@{\quad}p{8.5em}l@{\quad}p{8.5em}l@{\quad}p{8.5em}@{}}
\li|¬| & \verb|\not| &
\li|∧| & \verb|\and| &
\li|∨| & \verb|\or| \\
\li|→| & \verb|\->| &
\li|↔| & \verb|\<->| &
\li|∀| & \verb|\fo| \\
\li|∃| & \verb|\ex| &
\li|≤| & \verb|\<=| &
\li|≥| & \verb|\>=| \\
\li|≠| & \verb|\neq| &
\li|≈| & \verb|\~~| &
\li|×| & \verb|\x| \\
\li|∘| & \verb|\circ| &
\li|∅| & \verb|\empty| &
\li|∪| & \verb|\union| \\
\li|∩| & \verb|\intersect| &
\li|∈| & \verb|\in| &
\li|⇃| & \verb|\downleftharpoon| \\
\li|◯| & \verb|\bigcirc| &
\li|←| & \verb|\<-| &
\li|↦| & \verb|\mapsto| \\
\li|⇒| & \verb|\=>| &
\li|⟹| & \verb|\==>| &
\li|⟦| & \verb|\[[| \\
\li|⟧| & \verb|\]]| &
\li|α| & \verb|\a| &
\li|β| & \verb|\b|\\
\li|γ| & \verb|\g| &
\li|ε| & \verb|\e| &
\li|σ| & \verb|\s| \\
\li|₀| & \verb|\0| &
\li|₁| & \verb|\1| &
\li|₂| & \verb|\2| \\
\li|₃| & \verb|\3| &
\li|₄| & \verb|\4| &
\li|₅| & \verb|\5| \\
\li|₆| & \verb|\6| &
\li|₇| & \verb|\7| &
\li|₈| & \verb|\8| \\
\li|₉| & \verb|\9|
\end{tabular}
\end{center}

\vskip3\smallskipamount
