0 2025/lean-1105

Intro

Over the past while I’ve been learning about Lean, a functional programming language and proof assistant, and I wanted to share these cool insights about its type system and the overall big picture of what’s happening. While it is possible to use Lean to formalize math without going into the weeds, I thought this was pretty neat.

This will not attempt to be a tutorial, but I will try to show give you an understanding of the overall system and how to “correctly” think in Lean.

Types

First, let’s build some intuition for types. A type can be thought of as a set of terms, and we write (analogous to set membership with ), so for example . In Lean, however, types themselves are terms of another type! The type of types is also a type, but we need to avoid the type of all types that do not contain themselves, so these types are arranged in a hierarchy called “type universes”. So, we have , then , and and so on. Note that is really just shorthand for .

We can construct types by combining simpler types, and these types will inhabit the appropriate type universe. For example, we can have a function , and . In the same way, we can consider the type constructor as a function which takes any type to the type of lists of that type. Then, . In real Lean, List is polymorphic over type universes, meaning we can use List as if it were for any universe :

List.{u} (α : Type u) : Type u

With this, we are ready to take a look at the fundamental idea behind Lean as a theorem prover: propositions (like ) can be represented as types, and proofs of propositions can be represented as terms of that type (). This means that true propositions are the types with terms, and false propositions are types with no terms (you can never make an instance of that type). Thus, we can use type checking to prove theorems! Functions and algebraic data types correspond to logical operators, and this is something called the Curry-Howard correspondence:

Logic	Corresponding Type
Implication	Function type
For all	Dependent function type where
And	Product type
There exists	Dependent product type where
Or	Sum type
Truth	Unit type
Falsehood	Empty type
Negation	Function type

Implication is a function type because proving means constructing a proof of given a proof of . Proving means constructing both a proof of and a proof of . Etc. Etc.

Note that this is where the dependent part of the dependent type theory comes in: notice how in the dependent function types, the type of the return value depends on the value of the function input. We have also encountered , the type of propositions (i.e. ), and this type actually behaves kind of weirdly. It actually fits into our hierarchy of type universes at the beginning, so , and in fact is synonymous with (aka ), and is really just shorthand for .

We saw previously that building a new type out of types from a universe generally moves you one universe up from the max of the universes that appear (i.e. ), but that is not the case with . All the composite types that we have constructed above are all still propositions, so for example if a function type returns a , then it has type no matter the universe of its arguments.

One neat thing about propositions as types is that to assume an axiom is simply to assert that an object with a given type exists. Let’s take a look at one of the axioms that Lean assumes, propositional extentionality:

axiom propext {a b : Prop} : (a ↔ b) → a = b

The curly braces here signal that we have implicit arguments {a b : Prop} which Lean will automatically fill in for us. This says that if we have “a if and only if b”, then a and b are equal, and it implies functional extensionality:

theorem funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
    (h : ∀ x, f x = g x) : f = g := by sorry

This says that if two functions agree on all values, then they are equal, and we can construct a proof of this from propext, but that’s besides the point. This also means that any two proofs of the same proposition are considered equal, so all propositions are really either just the unit type or the empty type. Here, sorry is also an axiom, and it is actually a contradiction (it is an instance of the empty type, which by definition cannot have any instances) that can be used to prove anything (ex falso quodlibet!), and it is our way of telling Lean “sorry, I don’t have a proof yet, but just trust me”. How the heck does this work?

This actually ties back to the concept of initial and terminal objects (see my post on category theory), but the gist is that if a type is uninhabited, then there is exactly one function from that type to any other type. We think of functions as distinct ways of assigning a value of the output type to each value of the input type, so a there are distinct functions (for each , you have a choice from options). Thus, if , then there is exactly one way to do this: you don’t get to make any choices because there are zero instances of . We can always conjure up this function from an uninhabited type to any other type, and then sorry, as a (paradoxical) instance of an uninhabited type, allows us to use this function to create an instance of any other type, inhabited or not.

This also explains why we can model negation as : if were inhabited (i.e. it was true), then we would have to choose a value of the uninhabited type for each value of , which is impossible, so this function type is uninhabited. However if were uninhabited, we don’t have to choose anything by the argument above, so the type would be inhabited, proving . This also means that I guess.

Actually Using Lean

Almost every type is some combination of the types, dependent function types, and inductive types. For example, we can define sum and product types inductively:

inductive Prod (a : Type u) (b: Type v) where
| mk (l: a) (r: b): Prod a b

inductive Sum (a: Type u) (b: Type v) where
| inl (l: a): Sum a b
| inr (r: b): Sum a b

Here, our Prod type has one constructor, and you need both an object of type a and an object of type b to construct an object of type Prod a b. Its dual, Sum, has two constructors, allowing you to make an object of type Sum a b from either an object of type a or an object of type b. Of course, Prod and Sum are really functions on types:

Prod.{u, v} (a : Type u) (b : Type v) : Type (max u v)

We can also define True and False and the natural numbers in this way:

inductive True where
| mk: True

inductive False where

inductive Nat where
| zero: Nat
| succ (n: Nat): Nat

And we can use them with match statements and a few different ways to write functions:

/- explicit lambda -/
def f1: Sum Nat Nat → Nat := λ x ↦ match x with 
| Sum.inl y => y + 2
| Sum.inr y => y + 3

/- or write the parameter -/
def f2 (x: Sum Nat Nat): Nat := match x with
| Sum.inl y => y + 2
| Sum.inr y => y + 3

/- syntactic sugar -/
def f3: Sum Nat Nat → Nat
| Sum.inl y => y + 2
| Sum.inr y => y + 3

/- some familiar haskell stuff like $ is in Lean too -/
#eval f1 $ Sum.inl 4 /- gives 6 -/

Here, the #eval command compiles our code and runs it. We can also use #reduce, which does real type inference, but that is more expensive. Other useful commands include

• #check to look at the type of an expression
• #print axioms some_theorem to see what axioms your theorems are relying on. Do they cheat using sorryAx? Do they rely on the axiom of choice?

We can also package elements together into a structure similar to C/C++‘s struct.

structure Point where
  x: Nat
  y: Nat

#eval (Point.mk 1 2).x

Lean automatically defines the inductive type with the appropriate constructor (it’s really just a product type), and in Lean the .x syntax secretly translates to calling the function Point.x : Point → Nat on the point.

Now let’s try to do some math!

Doing Math in Lean

Ok that’s great, but how do you actually represent something like a group? For that, we use a structure (kinda) and do something like this:

class Group (R: Type u) where
  ident: R
  op: R → R → R
  inv: R → R

  assoc: ∀(a b c: R), op (op a b) c = op a (op b c)
  ident_cancel: ∀(a: R), op ident a = a
  inv_cancel: ∀(a: R), op (inv a) a = ident

An object of type Group R is a set of group operations acting on R together with a proof that they satisfy the group axioms. But wait, why did I say class and not structure? A class is simply a structure where Lean will automatically look for an instance without you having to pass the instance around explicitly everywhere. This is how Lean implements things like operator overloading, and it’s almost the exact same as how Rust does it. For example, the + operator is basically defined like this:

class Add (R: Type u) where
  add: R → R → R

instance: Add Nat where
  add (a: Nat) (b: Nat): Nat := match a with
    | Nat.zero => b
    | Nat.succ x => (myAdd x b).succ

/- and then define that a + b means Add.add a b -/

In Lean, you can actually just make instances of Add and HAdd and have your custom types automatically work with + as you’d expect. Classes can also extend other classes, so for example we could have done

class Group (R: Type u) extends Mul R where
  /- ... -/

and used a * b instead of op a b. Multiple inheritance is also supported, though idk the semantics of how Lean handles diamond inheritance. Even without making Group extend Mul, we can still define an instance and use * with our group elements (though this comes with some drawbacks):

instance {R} [G: Group R]: Mul R where
  mul := G.op 

Here, R and G are implicit arguments, and Lean will follow some rules to look for this instance when there’s an instance of Group R. We also could have explicitly named our instance by doing this (but we don’t have to name our instances):

instance my_instance {R} [G: Group R]: Mul R where /- ... -/

Another useful thing to know is that we can make implicit arguments explicit by writing an @, so we can write @my_instance R group_instance to explicitly refer to an implementation for a specific type and group structure.

Tactics and Theorem Proving

Actually proving theorems usually involves using tactics, and I won’t really be covering this because there already exist many Lean tutorials covering this. Instead, I will just leave you with some code that I wrote over the weekend to try to teach myself Lean. First a small note:

variable {R} [G: Group R]

is not really declaring a variable in the traditional sense. Instead, we effectively add those items as implicit arguments to every declaration in the current namespace/section, so in that way we can access those names in theorems, examples, defs, etc. There really is no big difference between all those things (including things like lemma and such), and they are all doing essentially the same thing just with slightly different connotations/semantics. theorem will give you a satsifying check mark when you manage to prove it. Anyways, here’s the code for your happy reading.

class Group (R: Type u) where
  ident: R
  op: R → R → R
  inv: R → R

  assoc: ∀(a b c: R), op (op a b) c = op a (op b c)
  ident_cancel: ∀(a: R), op ident a = a
  inv_cancel: ∀(a: R), op (inv a) a = ident

/- groups. sorry i don't have access to
   infix operators yet so this is a little painful -/
namespace Group
  variable {R} [G: Group R]

  theorem left_op_inj {b c}: ∀(a: R), G.op a b = G.op a c → b = c := by
    intro a hyp
    calc
      b = G.op G.ident b := by rw [G.ident_cancel]
      _ = G.op (G.op (G.inv a) a) b := by rw [G.inv_cancel]
      _ = G.op (G.inv a) (G.op a b) := by rw [G.assoc]
      _ = G.op (G.inv a) (G.op a c) := by rw [hyp]
      _ = G.op (G.op (G.inv a) a) c := by rw [← G.assoc]
      _ = c := by rw [(G.inv_cancel a), G.ident_cancel]

  @[simp]
  theorem cancel_ident (a: R): G.op a G.ident = a := by
    apply left_op_inj (G.inv a)
    calc
      _ = G.op (G.op (G.inv a) a) G.ident := by rw [G.assoc]
      _ = G.ident := by rw [G.inv_cancel, G.ident_cancel]
    rw [G.inv_cancel]

  @[simp]
  theorem cancel_inv (a: R): G.op a (G.inv a) = G.ident := by
    apply left_op_inj (G.inv a)
    calc
      _ = G.op (G.op (G.inv a) a) (G.inv a) := by rw [G.assoc]
      _ = G.op G.ident (G.inv a) := by rw [G.inv_cancel]
      _ = G.inv a := by rw [G.ident_cancel]
    symm
    rw [cancel_ident]

  @[simp]
  theorem ident_inv: G.inv G.ident = G.ident := by calc
    G.inv G.ident = G.op G.ident (G.inv G.ident) := by
      rw [G.ident_cancel]
    _ = G.ident := by rw [(cancel_inv G.ident)]

  @[simp]
  theorem inv_inv (a: R): G.inv (G.inv a) = a := by
    apply left_op_inj (G.inv a)
    rw [cancel_inv]
    rw [G.inv_cancel]

  theorem right_op_inj {b c}: ∀(a: R), G.op b a = G.op c a → b = c := by
    intro a hyp
    calc
      b = G.op b G.ident := by rw [cancel_ident]
      _ = G.op b (G.op a (G.inv a)) := by rw [cancel_inv]
      _ = G.op (G.op b a) (G.inv a) := by rw [G.assoc]
      _ = G.op (G.op c a) (G.inv a) := by rw [hyp]
      _ =  G.op c (G.op a (G.inv a)) := by rw [← G.assoc]
      _ = c := by rw [cancel_inv, cancel_ident]

  /- ok this is probably not the optimal solution but it works -/
  @[simp]
  theorem inv_dist (a b: R): G.inv (G.op a b) = G.op (G.inv b) (G.inv a) := by
    apply left_op_inj (G.op a b)
    symm
    rw [G.assoc]
    conv =>
      lhs; rhs;
      rw [← G.assoc, cancel_inv, ident_cancel]
    rw [cancel_inv]
    symm
    rw [cancel_inv]
end Group


class AbelianGroup (R: Type u) extends Group R where
  commute: ∀(a b: R), op a b = op b a

@[simp]
def abelian_commute {R} [G: AbelianGroup R] := G.commute


/- Not using mathlib for this! -/
class Field (R: Type u) extends Mul R, One R, Inv R where
  add: AbelianGroup R

  /- we expose the group structure later since we need to exclude 0 for some things -/
  mul_assoc: ∀(a b c: R), a * (b * c) = (a * b) * c
  mul_commute: ∀(a b: R), a * b = b * a
  mul_inv_cancel: ∀(a: R), (a ≠ add.ident) → a⁻¹ * a = 1
  mul_ident_cancel: ∀(a: R), 1 * a = a

  one_nez: 1 ≠ add.ident
  distribute: ∀(a b c: R),
    a * (add.op b c) = add.op (a * b) (a * c)

instance fieldAdd {R} [F: Field R]: Add R where
  add := F.add.op
instance fieldZero {R} [F: Field R]: Zero R where
  zero := F.add.ident
instance fieldNeg {R} [F: Field R]: Neg R where
  neg := F.add.inv

structure NonZero (α : Type u) (z : α) where
  val: α
  proof: val ≠ z

@[ext]
theorem nonzero_ext {α z} (a b: NonZero α z) (valeq: a.val = b.val): a = b := by
  cases a; cases b
  congr

section Field
  variable {R} [F: Field R]

  @[simp] theorem add_to_grp (a b : R):
    a + b = F.add.op a b := by rfl
  @[simp] theorem neg_to_grp (a : R): -a = F.add.inv a := by rfl
  @[simp] theorem zero_to_grp: 0 = F.add.ident := by rfl

  @[simp] def mul_assoc := F.mul_assoc
  @[simp] def mul_commute := F.mul_commute
  @[simp] def mul_ident_cancel := F.mul_ident_cancel
  @[simp] def one_nez: 1 ≠ 0 := by simp
  @[simp] def distribute: (a b c: R) →
    a * (b + c) = a * b + a * c := F.distribute

  /- it should not be this bad but this works -/
  @[simp]
  theorem zero_mult (a: R): 0 * a = 0 := by
    have eq: 0 * a = 0 * a + 0 * a := by
      calc
        _ = (0 + 0) * a := by simp
        _ = a * (0 + 0) := by rw [mul_commute]
        _ = a * 0 + a * 0 := by rw [add_to_grp (a * 0), ← F.distribute, add_to_grp]
        _ = 0 * a + 0 * a := by rw [mul_commute]

    let eq := congrArg (λ x => -(0 * a) + x) eq
    dsimp at eq
    rw [add_to_grp (-(0*a)), add_to_grp (-(0*a))] at eq
    rw [add_to_grp (0*a), neg_to_grp, ← F.add.assoc] at eq
    rw [F.add.inv_cancel, F.add.ident_cancel] at eq
    rw [← zero_to_grp] at eq
    symm; exact eq

  theorem mult_nz (a b: R): (a ≠ 0) → (b ≠ 0) → (a * b ≠ 0) := by
    intro anz bnz
    rw [zero_to_grp] at anz
    let contra: ¬(a * b ≠ 0) → False := by
      intro hyp
      simp at hyp
      let eq := congrArg (λ x ↦ a⁻¹ * x) hyp
      dsimp at eq
      rw [mul_assoc, F.mul_inv_cancel a anz, F.mul_ident_cancel] at eq
      rw [mul_commute, ← zero_to_grp, zero_mult a⁻¹] at eq
      let c: b = 0 ∧ b ≠ 0 := ⟨eq, bnz⟩
      simp at c
    exact Classical.byContradiction contra

  theorem inv_nz (a: R): (a ≠ 0) → (a⁻¹ ≠ 0) := by
    intro nz
    let contra: ¬(a⁻¹ ≠ 0) → False := by
      intro hyp
      simp at hyp
      let eq := congrArg (λ x ↦ a * x) hyp
      dsimp at eq
      rw [mul_commute, F.mul_inv_cancel a nz] at eq
      rw [mul_commute, ← zero_to_grp, zero_mult] at eq
      simp [F.one_nez] at eq
    exact Classical.byContradiction contra

  instance mulGrp: Group (NonZero R F.add.ident) where
    ident := NonZero.mk F.one F.one_nez
    op := fun a b ↦ NonZero.mk (F.mul a.val b.val) (mult_nz a.val b.val a.proof b.proof)
    inv := fun x ↦ NonZero.mk (x.val⁻¹) (inv_nz x.val x.proof)
    assoc := by
      intro a b c
      ext; dsimp
      symm; exact (F.mul_assoc a.val b.val c.val)
    ident_cancel := by
      intro a
      ext; dsimp
      exact (F.mul_ident_cancel a.val)
    inv_cancel := by
      intro a
      ext; dsimp
      exact (F.mul_inv_cancel a.val a.proof)

  theorem zero_spreads (a b: R): (a = 0) ∨ (b = 0) → (a * b = 0) := by
    intro hyp
    match hyp with
    | Or.inr aez => rw [aez, mul_commute]; exact zero_mult a
    | Or.inl bez => rw [bez]; exact zero_mult b

end Field

/- (inhabited) Module over a Field :) -/
class VectorSpace {R} (V: Type u) (F: Field R) extends Add V, HMul R V V, Inhabited V where
  vect_dist: ∀(r: R)(u v: V), r * (u + v) = r * u + r * v
  field_dist: ∀(r s: R)(u: V), (r + s) * u = r * u + s * u
  mul_eq: ∀(r s: R)(u: V), (r * s) * u = r * (s * u)
  ident: ∀(u: V), F.one * u = u

/- a field is a vector space -/
instance V0 {R} [F: Field R]: VectorSpace R F where
  default := F.one
  vect_dist := F.distribute
  field_dist := by
    intro r s u
    rw [F.mul_commute, distribute, F.mul_commute, F.mul_commute u s]
  mul_eq := by intro r s u; symm; apply F.mul_assoc
  ident := by intro u; apply F.mul_ident_cancel

/- the product of two vector spaces over the same field is a vector space. i'm gonna have to prove that the cartesian product is associative aren't i? ugh -/
instance ProdSpace {R V1 V2} [F: Field R] (v1: VectorSpace V1 F) (v2: VectorSpace V2 F): VectorSpace (V1×V2) F where
  add (a b : V1 × V2) := ⟨v1.add a.fst b.fst, v2.add a.snd b.snd⟩
  hMul (s : R) (v : V1 × V2) := ⟨v1.hMul s v.fst, v2.hMul s v.snd⟩
  vect_dist := by
    intros
    sorry
  field_dist := by sorry
  mul_eq := by sorry
  ident := by sorry

def Injective {X Y} (f: X → Y) :=
  ∀(a b: X), f a = f b → a = b

def Surjective {X Y} (f: X → Y) :=
  ∀(b: Y), ∃(a: X), f a = b

structure LinFun {X Y R} [F: Field R] (vx: VectorSpace X F) (vy: VectorSpace Y F) where
  f: X → Y
  linadd: ∀(u v : X), f (u + v) = f u + f v
  linmul: ∀(u: X)(α: R), f (α * u) = α * f u


instance linearZero {R X Y} [F: Field R] (vx: VectorSpace X F) (vy: VectorSpace Y F): LinFun vx vy where
  f (x: X) := vy.hMul 0 vy.default
  linadd := by sorry
  linmul := by sorry

/- the space of linear maps is a vector space -/
instance MapSpace {X Y R} [F: Field R] (vx: VectorSpace X F) (vy: VectorSpace Y F): VectorSpace (LinFun vx vy) F where
  add := sorry
  hMul := sorry
  default := linearZero vx vy
  vect_dist := sorry
  field_dist := sorry
  mul_eq := sorry
  ident := sorry

---

Log in to Comment

Firebase not Loaded

---