I've been wanting to learn the basics of Lean recently. I'm curious if I would find it useful while learning or doing math, and I also just want to know more about formal verification. I'm going to try out a Julia Evans-style—"Here's this thing I learned about and what I think is cool"—post with my initial thoughts.

I'm starting with the Theorem Proving in Lean 4 guide, as it seemed most relevant among the beginner resources.

Lean is a functional programming language that is used for formal verification; it functions both as an Interactive Proof Assistant and as an Automated Theorem Prover.

Interactive Proof Assistants allow you to define a set of objects and then prove statements about the objects using logic. This could be proving that hardware or software meets a specification, or proving mathematical theorems. The allure here is that the system guarantees soundness for us: if our theorem gets that blue checkmark, then we know it is true (as it's written at least, Lean can't preclude incorrectly defined goal statements).

Automated theorem proving tools help with finding these proofs.

Lean at 10,000 feet

Here's my understanding of how the different bits of the lean language map to formal verification:

Lean's type system: allows us to create mathematical objects, and serve as the foundation for verification
Propositions: allow us to model logic (through typechecking, as we'll see)
Predicates, Quantifiers, and Equality: bridge the two and allow us to make propositions about objects
Tactics: automated theorem proving tools that make writing forma proofs tenable

There are a fair amount of fancy terms thrown around for how Lean works: "Calculus of Constructions", "Dependent Type Theory", "Propositions as Types", "Curry-Howard Isomorphism", etc.

Here's my current understanding.

Lean has a Dependent Type System

Lean's type system is a Dependent Type System, which seems to mean the output type of a function can rely on the value of an input. In the below snippet, the function cons takes in a Type for its first parameter, which the remaining parameters then depend on, and then returns something of type List α, where α could be Nat, Vector .., etc..

def cons (α : Type) (a : α) (as : List α) : List α :=
  List.cons a as

Propositions as Types

With the type system, we can define our own types that represent mathematical objects.

A special type is Lean's Prop. Each instance of Prop represents a statement that can be true or false. The Curry-Howard Isomorphism (aka propositions as types) is a neat observation that the typechecking systems of programming languages can be used to represent mathematical logic.

How do we represent when a proposition is true? In Lean, prepositions are themselves types. A proposition p : Prop is true if there is an expression t that is of type p, i.e. t : p. The expression t is a proof.

Here is an example:

-- define p and q to be propositions
variable {p q: Prop}

-- given p and q are true, p is true
theorem t1: p → q → p := fun hp : p => fun hq : q => hp

We can see that theorem t1 is in fact a function. It takes in two propositions, p and q, and returns a proposition q. Lean tells us that this theorem is true because the expression we provide as the body typechecks to the signature p → q → p.

This is pretty cool! Here's one more example (there are plenty more here):

theorem contrapositive (hpq: p → q) (hnq: ¬q) : ¬p :=
  fun hp: p =>
  show False from hnq (hpq hp)

Negations are represented as a functions that send a prop to False, and here we're constructing a function that sends p to False by first applying hpq to hp, giving q and then combining that with ¬q to yield a contradiction.

Quantifiers and Equality

In order to make statements about objects that aren't propositions, we need a way to create propositions about objects. If α : Type is some object, then p: (x : α) → Prop is a proposition on α.

For example:

def Even (n : Nat) : Prop :=
	n % 2 = 0

Notice that Even doesn't hold for every Nat. This means there exists some (n : Nat) such that there are no expressions that typecheck to Even n.

Implicit here is the fact that ((x : α) → Prop) : Prop) (functions that map objects to propositions are themselves propositions). This is true because Prop is special compared to other types, in a way that apparently resolves the issues that arise when a set can contain itself (probably should look more at this later).

Universal ($\forall$) and existential ($\exists$) quantifiers are also represented as types:

∀x : α, p x is the same as (x : α) → p x; if there exists an expression (proof) for each element of α for this proposition, it means there is this mapping.
∃x : α, p x is the same as a concrete pair of an element, x: α, and a proof that the proposition holds for that element, h : p x.

Also interesting is equality. Equality is reflexive, transitive, and symmetric:

variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd

But it's also stronger than the typical equality in programming languages in that if I have a = b and p a, then I also have p b. In other words, we can substitute equal expressions without changing the truth value.

Tactics

Tactics are automations that help search the space of potential expressions (proofs) to find one of a certain type (thus accomplishing a goal). Of course, any proof that uses tactics can also be done without those tactics, as we know the full expression exists.