import Mathlib.Data.Nat.Basic -- For natural numbers
import Mathlib.Data.Int.Basic -- For integers
import Mathlib.Data.List.Basic -- For lists
import Mathlib.Data.Vector -- For vectors
import Mathlib.Logic.Basic -- For logical operations
import Mathlib.Data.Set.Basic -- For set operationsAt the very base of mathematics, we have the concept of sets, which are collections of objects. Set theory provides a formal language for defining and manipulating these collections. Set theory forms the programming language of mathematics, allowing us to express mathematical concepts and operations in a precise and unambiguous way. All mathematical structures can be built from sets, and all machinery operating on these structures can be expressed in terms of set operations. Mathematics is built on a foundation of axioms and rules that define the basic concepts and operations used in mathematical reasoning. These foundations provide a framework for proving theorems and establishing the validity of mathematical results.
Set theory, however, is not the only foundational system for mathematics. Over the past century, another foundational system has emerged: type theory. Type theory is a formal system that classifies mathematical objects by their types and specifies valid operations on these objects. In type theory, every mathematical object has a type, and types serve multiple roles, such as classifying objects, specifying operations, catching errors, and representing propositions. Type theory provides a different perspective on mathematics, emphasizing the structure of mathematical objects and the relationships between them.
While both set theory and type theory can serve as foundations for mathematics, they approach mathematical reasoning in fundamentally different ways. Lean, like several other modern proof assistants, is based on type theory. This choice enables Lean to provide powerful tools for both mathematical reasoning and computation. Practically, using Lean, and hence type theory, instead of set theory implies we can automatically check proofs, instead of the ultra-tedious manual checking that would be required in set theory. This is because Lean’s type theory is designed to be computable, which means that we can write programs that manipulate proofs and terms. This is a significant advantage over set theory, where proofs are typically written in natural language and must be checked manually by humans, who tend to make their own mistakes.
In set theory, mathematical objects are sets. Here we cover the very basics of sets and their operations.
Sets can be constructed by enumerating their elements. For example, x is a set containing the natural
numbers 1, 2, and 3:
def y : Set Nat := {1, 2, 3} -- y is the set {1, 2, 3}Sets can also be constructed by the builder notation {x | P x}, where P x is a predicate that specifies the objects
that belong to the set. For example, x is a set of natural numbers greater than 0:
def x : Set Nat := {n | n > 0} -- x is the set of natural numbers greater than 0Set membership is denoted by the symbol ∈. It implies that an object, x, belongs to a set, for example
here x belongs to the set of natural numbers Nat:
def x : Set Nat := {n | n > 0} -- x is the set of natural numbers greater than 0Subsets are denoted by the symbol ⊆. It implies that a set, y, is a subset of another set,
x:
def y : Set Nat := {n | n > 1} -- y is the set of natural numbers greater than 1
def z : Bool := y ⊆ x -- z is true because y is a subset of xSets can be combined using set operations. For example, the union of two sets x and y is a
set containing all elements that belong to either x or y:
def x : Set Nat := {1, 2, 3} -- x is the set {1, 2, 3}
def y : Set Nat := {3, 4, 5} -- y is the set {3, 4, 5}
def z : Set Nat := x ∪ y -- z is the union of x and ySimilarly, the intersection of two sets x and y is a set containing all elements that
belong to both x and y:
def z : Set Nat := x ∩ y -- z is the intersection of x and ySets can have complements, which are the elements that do not belong to the set:
def z : Set Nat := xᶜ -- z is the complement of xThere is a special set, the empty set, denoted by ∅, which contains no elements:
def z : Set Nat := ∅ -- z is the empty setand power sets, which are sets of all subsets of a given set:
def z : Set (Set Nat) := 𝒫 x -- z is the power set of xThe operations on sets have several properties. For example, the following properties hold for union and intersection:
def x : Set Nat := {1, 2, 3}
def y : Set Nat := {3, 4, 5}
#check x ∪ y -- Set Nat
#check y ∪ x -- Set NatHere, \(z_{1}\), \(z_{2}\), and \(z_{3}\) are equivalent.
def z : Set Nat := {5, 6, 7}
#check x ∪ (y ∪ z) -- Set Nat
#check (x ∪ y) ∪ z -- Set NatHere, \(z_{1}\) and \(z_{2}\) are equivalent.
#check x ∪ (y ∩ z)
#check (x ∪ y) ∩ (x ∪ z)Here, \(z_{1}\) and \(z_{2}\) are equivalent.
#check x ∪ x
#check x ∩ xHere, \(z_{1}\) and \(z_{2}\) are equivalent to \(x\).
def z₁ : Set Nat := x ∪ ∅
def z₂ : Set Nat := x ∩ {n | n > 0}Here, \(z_{1}\) is equivalent to \(x\) and \(z_{2}\) is equivalent to \(x\).
def z₁ : Set Nat := x ∪ (y ∩ z)
def z₂ : Set Nat := (x ∪ y) ∩ (x ∪ z)Here, \(z_{1}\) and \(z_{2}\) are equivalent.
Additional properties of set operations exist and are fundamental to mathematical reasoning, but we omit them as they fall outside this book’s scope.
Type theory provides an alternative foundation for mathematics and computer science, distinct from set theory. Rather than constructing everything from sets, type theory centers on the concept of types, with the fundamental principle that every object has a type. This computational emphasis makes type theory well-suited for formal verification and automated proof checking, as implemented in proof assistants like Lean.
The core building blocks of type theory are:
Nat (natural numbers) or Bool (booleans). But types can be much more sophisticated,
representing functions, propositions, and complex data structures.5 is a term
of type Nat, and true is a term of type Bool. We use the notation
a : A to say that term a has type A.This judgment asserts that something is a well-formed type. In Lean:
#check Nat -- Nat : Type
#check Bool -- Bool : Type
#check Nat → Bool -- Nat → Bool : Type (Functions from Nat to Bool)Formally, the judgment A : Type (or sometimes A type, depending on the specific type
theory) means that A is a valid type. This is not something you prove within the system; it’s a
foundational assertion established by rules. The notation #check will only succeed for well formed
types.
This judgment asserts that a term belongs to a specific type:
#check (5 : Nat) -- 5 : Nat
#check (true : Bool) -- true : Bool
def myNumber : Nat := 5
#check myNumber -- myNumber : Nat
-- Example of an ill-typed term (this would cause an error):
-- def badNumber : Nat := true -- Error: type mismatchFormally, a : A means “term a has type A”. Again, this is not a proposition to
be proven, but a declaration based on the rules of type theory. Lean’s type checker enforces these rules. If you try to
construct a term that violates the typing rules, Lean will report an error.
This judgment asserts that two types are definitionally equal. This is a very strong form of equality. It means they
are the same type, not just equivalent in some way. This is often written as A ≡ B or (in some contexts)
just A = B (but be careful – in a type theory, equality can mean different things). Lean handles
definitional equality internally.
-- Example (though Lean infers this automatically)
def MyType : Type := Nat
#check MyType -- MyType : Type, which is definitionally equal to Nat.In this simple case, the type MyType on the right hand side is defined as equal to the Nat.
With a simple equality, this is a definitional equality. Other examples are provided below.
This judgment has two main forms, with critical distinctions:
2 + 2 and 4 are definitionally equal. Lean checks this
automatically.example : 2 + 2 = 4 := rfl -- Success! 2 + 2 and 4 are definitionally equal.rfl (reflexivity) works precisely because 2 + 2 and 4 are
definitionally equal. Lean can see this directly, without further proof steps.
a = b (where a and b are terms of the
same type) is itself a type! This is where the propositions-as-types principle comes in (which we’ll
cover later, but it’s good to be aware of it early). Proving a = b involves constructing a term of
that type.-- An easy example, still provable by rfl because of definitional equality
example : (2 + 2 : Nat) = (4 : Nat) := rfl
-- A slightly more interesting example, requiring a proof (using theorems)
example (n : Nat) : n + 0 = n := Nat.add_zero nCrucially, definitional equality implies propositional equality, but not the other way around. If
a ≡ b, then a = b is trivially provable (with rfl).
Type Theory has found extensive applications in computer science:
While Set Theory remains the most common foundation for mathematics, Type Theory offers some advantages: