Theorem Proving in Lean - Basics of Dependent Type Theory

The master guide is here.

DTT and its Specific Variant for Lean

Dependent type theory (DTT) allows you to express complex mathematical assertions and reason about them in a "natural and uniform" way. Lean is based on a version of DTT called the Calculus of Constructions, with a "countable hierarchy of non-cumulative inverses and inductive types". This sounds complex. The following section explains this.

First, let's talk Simple Type Theory

In "type theory" every expression has a specific type. e.g. the expression x+0 may denote a natural number in a specific context. In another context, it may be a floating point number, of a particular precision.

In Lean, a natural number is an arbitrary precision unsigned integer.

An arbitrary-precision integer can grow to any number of bits, limited only by available memory. This differs from so-called fixed-width integers (8-, 32-, 64- bit).  A variable-length array of digits/bits are used so it can represent arbitrarily large integers without overflow. (Analogy: BigInt in Java, or System.Numerics.BigInteger in C#).

Let's define some constants in Lean.

/- Define some constants. -/

def  m:  Nat := 1   --m is a natural number

def  n :  Nat := 0

def  b1: Bool := true  --b1 is a Boolean

def  b2: Bool := false

Now check their types using: #check m;  #check n; #check n+0 etc. You can also run some "evals" in Lean: #eval  5*4; #eval m+2 etc.

The def keyword introduces new constant symbols to the working environment. The #check command asks Lean to report their types. The #eval command asks Lean to evaluate the given expression.

What makes simple type theory powerful is you can build new types out of others.