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

Success stories

Mathematics:

Computer science:

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:

A selection of popular proof assistants

Classified by logical foundations

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)

Strengths:

Lean at VU Amsterdam:

Lean specifications

In a first approximation:

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

For typed functional programming:

Acknowledgment

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