Skip to content
Theo Bains
Menu
All projects

academic project

Building Mathematics with Lean

A summer research project using Lean to derive mathematical structures from basic axioms and formally verify proofs.

Lean 4 guided proof explorer

Lean proof walkthrough

This is a teaching trace through pre-authored proofs. Use the control below to switch theorems; the source, goal, and explanations update immediately.

Active theorem

Compose two implications by passing evidence through them in order.

Lean 4 source

Lines 1-5

theorem implication_comp    (P Q R : Prop)    (h₁ : P → Q)    (h₂ : Q → R) :    P → R := by  intro hp  exact h₂ (h₁ hp)

Lean 4 InfoView

Step 1 of 3

Start

Local context

  • P Q R : Prop
  • h₁ : P → Q
  • h₂ : Q → R

Current goal

Step explanation

What changed

The implication in the goal has not yet been introduced.

Why it works

We need to show that assuming P lets us produce R.

This is a pre-authored teaching trace, not a Lean runtime. It does not execute or verify arbitrary proof text.

Basic explanation

Lean 4 is an interactive theorem prover: you propose a proof, and the system checks that every step follows from the declared axioms and assumptions. It behaves like a strict compiler for mathematics - ideas remain human, but gaps and hidden leaps are rejected.

Under the Curry-Howard correspondence, a proposition is a type and a proof is a program inhabiting that type. Proving P∧Q→PP \land Q \to P means writing a function that accepts a pair of evidence and returns the first component. That discipline scales from tiny lemmas to larger constructive developments.

Context

This was an individual summer research project affiliated with the University of Liverpool, focused on building mathematical structure from small logical foundations inside Lean rather than trusting informal sketches. The interactive explorer on this page is a pre-authored teaching trace of representative tactics - not a live Lean server - but it mirrors the InfoView style of stepping through goals, context, and justifications.

Method

Work proceeds by stating a theorem, inspecting the goal, and applying tactics (intro, exact, cases, induction, simp, …) that transform the proof state. Feedback from the elaborator forces precise specifications: if a term’s type does not match the goal, the proof does not close.

The explorer includes compact propositional examples (implication composition, conjunction symmetry), a natural-number induction identity, and a denser case-split proof distributing conjunction over disjunction. Use Choose a proof in the demo to switch theorems; the source highlight, local context, and explanations update together.

What this demonstrates

Formal verification makes refactoring a logical interface problem: change a lemma’s statement and every dependent proof must be repaired. That habit - specification, decomposition, and compiler-guided repair - transfers directly to careful software design and to the kind of rigorous argument expected in theoretical computer science.