1. Introduction

These are lecture notes for COMP2065: Introduction to formal reasoning. The main goal is to teach formal logic using an interactive proof system called Lean. You will be able to use predicate logic to make precise statements and to verify them using a proof system. The covers both statements in Mathematics and statements about computer programs, e.g. their correctness.

1.1. Interactive proof systems

Interactive proof systems have been used in the past to verify a number of interesting statements, for example the four colour theorem (that every map can be coloured with 4 colour) and the formal correctness of a optimising C compiler. The formal verification of hardware like processors is now quite standard and there is a growing number of software protocols being formally certified. In academia it is now common to accompany a paper in theoretical computer science with a formal proof to make sure that the proofs are correct. Mathematicians are just starting to verify their proofs.

Even if you are not going to use formal verification, it is an important part of a computer science degree to have some acquaintance with formal logic, either to read formal statements made my others or by being able to express facts precisely without ambiguity. I believe that the best way to learn logic these days is by using an interactive proof system because this removes any ambiguity on what constitutes a proof and also you can play with it on your own without the need of a teacher or tutor.

An interactive proof system is not an automatic theorem prover. The burden to develop a correct proof is on you, the interactive proof systems guides you and makes sure that the proof is correct. Having said this, modern proof assistants offer a lot of automatisation which enables to user not to have to get bogged down in trivial details. However, since our goal is to learn proofs, at least initially we won’t use much automatisation. It is like in Harry Potter, to be allowed to use the more advanced spells you first have to show that you master the basic ones.

1.2. Lean

Many interactive proof systems are based on Type Theory, this is basically a functional programming language with a powerful type system that allows us to express propositions as types and proofs as programs. A well known example is the Coq system which was developed (and still is) in France. However, we will use a more recent system which in many respects is similar to Coq, this is Lean which was (and is) developed under the leadership of Leonardo de Moura at Microsoft Research. Leonardo is famous for his work on automatic theorem proving, he developed the Z3 theorem prover. Lean’s goal is to connect automatic and interactive theorem proving. The system is called Lean because it only relies on a small core of primitive rules and axioms to make sure that it is itself correct.

Lean is available for free from https://leanprover.github.io/download/ It will be already installed on the lab machines (I hope). You can use it either via Microsoft’s Visual Code Studio or via emacs using lean mode. Yet another way to use lean is via a browser based version we will also use in the online version of these lecture notes.

Here is an example of a simple proof in Lean: we show that the sum of the first n odd numbers is the square of n. (Actually this example already uses some advanced magic in form of the ring tactic).

try it!

def sum_ℕ : ℕ → (ℕ → ℕ) → ℕ
| zero f := 0
| (succ n) f := f n + sum_ℕ n f

def nth_odd (i : ℕ) : ℕ :=
  2*i+1

#reduce (nth_odd 3)

#reduce (sum_ℕ 5 nth_odd)

theorem odd_sum : ∀ n : ℕ , sum_ℕ n nth_odd = n^2 :=
begin
  assume n,
  induction n with n' ih,
  refl,
  calc
    sum_ℕ (succ n') nth_odd
    = 2*n'+1+ sum_ℕ n' nth_odd : refl _
    ... = 2*n'+1+n'^2 : by rw ih
    ... = (n' + 1)^2 : by ring,
end

If you read this online, you can just click try it! which should transport you to the web interface. You need to wait until the orange text Lean is busy is replaced by a green Lean is ready (which may take a while depending on your computer, especially the 1st time).

You can put the cursor in the proof to see what the proof state is and you can evaluate the expressions after #reduce and maybe change the parameters. You can also change the proof (maybe you have a better one) or do something completely different (but then don’t forget to save your work by copy and paste). While you can work using the browser version only, for bigger exercises it may be better to install Lean on your computer.

The Lean community is very active.If you want to know more about Lean and it’s underlying theory, I recommend book Theorem Proving in Lean [AvMoKo2015] whose online version also uses the web interface. Actually if you notice that these lecture notes and the book use a very similar format then this is because I have stolen their setup (on the suggestion of one of the authors). Another useful book is The Hitchhiker’s Guide to Logical Verification [BaBeBlHo2020] (this is material for an MSc course at the University of Amsterdam) which goes beyond this course. A good place for questions and discussions is the Lean zulip chat (https://leanprover.zulipchat.com/) but please don’t post your coursework questions anywhere on social networks — this is considered academic misconduct. And yes, we do have staff members who can read other languages than English.

[AvMoKo2015]

Jeremy Avigad, Leonardo de Moura and Soonho Kong Theorem proving in Lean Microsoft Research, 2015, https://leanprover.github.io/theorem_proving_in_lean/

[BaBeBlHo2020]

Anne Baanen, Alexander Bentkamp, Jasmin Blanchette and Johannes Hölzl, The Hitchhiker’s Guide to Logical Verification, 2020, https://leanprover-community.github.io/learn.html