# 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](https://www.microsoft.com/en-us/research/people/leonardo/) (Microsoft Research) since 2013
Its mathematical library is developed under the leadership of [Jeremy Avigad](http://www.andrew.cmu.edu/user/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](https://lean-forward.github.io/lean-together/2019/) meeting
* [Lean Forward](https://lean-forward.github.io) 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!_](http://learnyouahaskell.com/chapters)
## Demo
[`11_lecture.lean`](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_](https://leanprover.github.io/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!_](http://learnyouahaskell.com/chapters), 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