Lecture 1.1: Basics — Definitions and Propositions

We introduce the basics of Lean and proof assistants, without trying to carry out actual proofs yet

We focus on specifying objects and statements of their intended properties

Proof assistants

Also called interactive theorem provers

They

check and help develop formal proofs
can be used to prove big theorems, not only logic puzzles
can be tedious to use
are highly addictive (think video games)

Success stories

Mathematics:

the Mizar Math Library (in Mizar)
the four-color theorem (in Coq)
the odd-order theorem (in Coq)
the Kepler conjecture (in HOL Light and Isabelle/HOL)
the homotopy type theory libraries (in Agda, Coq, and Lean)
the Lorenz attractor (in Isabelle/HOL)

Computer science:

hardware and systems (e.g., floating-point arithmetic, microkernels, hardware memory models)
process calculi and programming language theory (e.g., semantics, software memory models, type systems, binder syntax)
program analysis (e.g., compilers, interpreters, static analyzers)
provers and solvers (e.g., proof assistants, automatic theorem provers, decision procedures, termination and confluence of term-rewriting systems)
security (e.g., cryptographic protocols, cryptography, information flow)

Kinds of proofs

Formal proof = proof expressed in a logical formalism, often developed using a proof assistant

Informal proof = pen-and-paper (or LaTeX) proof

Rigorous proof = thorough informal proof

Too many proofs look more like LSD trips than coherent mathematical arguments

Logical foundations

Three main (families of) logical foundations:

set theory
simple type theory (= higher-order logic)
dependent type theory

A selection of popular proof assistants

Classified by logical foundations

set theory: Isabelle/ZF, Metamath, Mizar
simple type theory: HOL4, HOL Light, Isabelle/HOL
dependent type theory: Agda, Coq, Lean, Matita

Hard to classify: ACL2 (Lisp-like first-order logic), PVS (simple type theory with dependent types and subtyping)

Pioneering system: AUTOMATH (by Nicolaas de Bruijn)

Lean

A new proof assistant developed primarily by Leonardo de Moura (Microsoft Research) since 2013

Its mathematical library is developed under the leadership of Jeremy Avigad (Carnegie Mellon University)

we use version 3.4.1 (likely the last release before Lean 4)
as a rule, we will rely only on its basic libraries and avoid depending on mathlib
this is a research project, with some rough edges

Strengths:

highly expressive logic based on the calculus of (inductive) constructions (a dependent type theory), abbreviated CIC or CoC
extended with classical axioms and quotient types
metaprogramming framework (to program custom proof automation)
white-box proof automation (in development)
modern user interface
documentation
open source

Lean at VU Amsterdam:

Lean Together 2019 meeting
Lean Forward project (2019–2023)

Lean specifications

In a first approximation:

CIC = typed functional programming + logic

In this lecture, we cover inductive datatypes, recursive functions, and lemma statements

If you are not familiar with typed functional programming (e.g., Haskell, ML, OCaml, Scala), we recommend that you study a tutorial, such as Learn You a Haskell for Great Good!

Demo

11_lecture.lean

Syntax seen so far

Declarations

Keyword	Description
`def`	defines a constant or function (possibly recursively)
`inductive`	introduces a (possibly recursive) type and its constructors
`lemma`	states a theorem
`structure`	introduces a record type and its projection functions
`namespace` ... `end`	puts all declarations in a named scope (to avoid name clashes)

Diagnosis commands

Command	Description
`#check`	prints type of a term
`#print`	prints definition of a constant or function
`#reduce`	computes the normal form of a term
`#eval`	executes a term; use it when `#reduce` fails

References

Theorem Proving in Lean, Chapter 1, Sections 7.1, 7.2, 7.4, 7.5, 8.1–8.3, Chapter 9

For typed functional programming:

Learn You a Haskell for Great Good!, especially Chapters 1 to 6

Acknowledgment

These notes are partly inspired by Tobias Nipkow's Concrete Semantics and Femke van Raamsdonk's Logical Verification courses