import Mathlib

-- A polynomial identity
example (x y : ℝ) :
    (x + y)^2 =
      x^2 + 2*x*y + y^2 := by
  ring

-- A statement and its proof
theorem add_zero_demo (n : ℕ) :
    n + 0 = n := by
  rfl

-- Assumptions used by the proof
#print axioms add_zero_demo

What is this about

Formal verification (of mathematical theorems)

• Write a mathematical statement and its proof in a precise language.
• A computer checks that the proof follows from the definitions and assumptions.
• Related: software verification. (Not the focus of this class.)
• Translation: mathematics ↔︎ logic ↔︎ computer science
• Lean 4: a proof assistant and a programming language.

Details: What is Lean? · Mathematics in Lean

import Mathlib

-- A polynomial identity
example (x y : ℝ) :
    (x + y)^2 =
      x^2 + 2*x*y + y^2 := by
  ring

-- A statement and its proof
theorem add_zero_demo (n : ℕ) :
    n + 0 = n := by
  rfl

-- Assumptions used by the proof
#print axioms add_zero_demo

Some historical successes -- 4CT

4-color theorem: every finite simple planar graph is 4-colorable.

• 1976: Appel & Haken, with Koch. Proof combining mathematics and computer calculations.
• 1997: Robertson, Sanders, Seymour & Thomas. A simpler proof, still using a computer.
• 2005: Gonthier, building on work with Werner. Formal proof in Coq (now Rocq).
• The formal proof checks the mathematical argument as well as the computations.

Details: Gonthier, Formal Proof: The Four-Color Theorem (2008)

import Mathlib

-- A polynomial identity
example (x y : ℝ) :
    (x + y)^2 =
      x^2 + 2*x*y + y^2 := by
  ring

-- A statement and its proof
theorem add_zero_demo (n : ℕ) :
    n + 0 = n := by
  rfl

-- Assumptions used by the proof
#print axioms add_zero_demo

Some historical successes -- Kepler's conjecture

Kepler's conjecture: the usual pyramid of equal balls has the largest possible packing density in 3D.

• 1998: Hales, with Ferguson, announces a proof involving extensive computation.
• Refereeing the mathematical argument and all the computer calculations proves difficult.
• 2014: the Flyspeck project completes a formal proof.
  • Uses HOL Light and Isabelle.

Details: Hales et al., A formal proof of the Kepler conjecture · Flyspeck code

import Mathlib

-- A polynomial identity
example (x y : ℝ) :
    (x + y)^2 =
      x^2 + 2*x*y + y^2 := by
  ring

-- A statement and its proof
theorem add_zero_demo (n : ℕ) :
    n + 0 = n := by
  rfl

-- Assumptions used by the proof
#print axioms add_zero_demo

Recent successes in Lean

• 2023: Polynomial Freiman--Ruzsa (PFR) over F₂ⁿ.
  • A new theorem in additive combinatorics, formalized within weeks of its proof.
  • Gowers, Green, Manners & Tao's mathematics; a collaborative Lean project.
• 2026: sphere packing in dimension 8.
  • Viazovska's optimality theorem for the E₈ lattice, checked by Lean.
  • Human formalizers + Gauss; work on readable, reusable code continues.

Details: PFR project · Tao's account · Sphere packing: the team's account

import Mathlib

-- A polynomial identity
example (x y : ℝ) :
    (x + y)^2 =
      x^2 + 2*x*y + y^2 := by
  ring

-- A statement and its proof
theorem add_zero_demo (n : ℕ) :
    n + 0 = n := by
  rfl

-- Assumptions used by the proof
#print axioms add_zero_demo

Fermat's last theorem -- now formalized

xⁿ + yⁿ = zⁿ has no solution in positive integers for integer n > 2.

• 1995: Wiles and Taylor--Wiles publish the proof.
• 4 September 2026: Anthropic releases a complete Lean formalization.
  • Claude agents, human guidance, and existing community libraries.
  • Follows the Darmon--Diamond--Taylor exposition of Wiles's argument.
• About 13 million lines of Lean. The release reports kernel and independent checks.
• A verified proof artifact and a readable mathematical exposition serve different purposes.

Details: Announcement and attribution · Code, theorem statement and verification

import Mathlib

-- A polynomial identity
example (x y : ℝ) :
    (x + y)^2 =
      x^2 + 2*x*y + y^2 := by
  ring

-- A statement and its proof
theorem add_zero_demo (n : ℕ) :
    n + 0 = n := by
  rfl

-- Assumptions used by the proof
#print axioms add_zero_demo

ATP vs ITP

Automated vs interactive theorem proving

• ATP: give the system a goal and assumptions; it searches for a proof.
• ITP: develop a proof interactively, with the computer checking each step.
• In practice, we combine them: choose the main ideas and automate routine steps.
• In Lean, tactics construct proofs that the kernel checks.
• AI can also propose steps or whole proofs for Lean to check.

Details: Lean: tactic proofs · Lean: proof validation

import Mathlib

-- A polynomial identity
example (x y : ℝ) :
    (x + y)^2 =
      x^2 + 2*x*y + y^2 := by
  ring

-- A statement and its proof
theorem add_zero_demo (n : ℕ) :
    n + 0 = n := by
  rfl

-- Assumptions used by the proof
#print axioms add_zero_demo

Some interactive theorem provers

Name	Origins / milestones
Mizar	Project begun in 1973
Isabelle	In use since 1986
Coq / Rocq	Begun in 1984; renamed Rocq in 2025
Lean	Begun in 2013; Lean 4 released in 2023

• Different foundations, libraries and styles of interaction.
• We will use Lean 4 + mathlib.

Details: Isabelle's early history · Coq's early history

import Mathlib

-- A polynomial identity
example (x y : ℝ) :
    (x + y)^2 =
      x^2 + 2*x*y + y^2 := by
  ring

-- A statement and its proof
theorem add_zero_demo (n : ℕ) :
    n + 0 = n := by
  rfl

-- Assumptions used by the proof
#print axioms add_zero_demo

Levels of help & automation

• Write a proof directly.
• Write a program that constructs a proof: tactics.
• Use specialized automation:
  • simp: simplify using known equalities and equivalences.
  • ring: polynomial identities; omega: linear integer arithmetic.
  • aesop, grind: more general proof search and reasoning.
• Mix explicit mathematical steps and automation as needed.

import Mathlib

example (x y : ℝ) : (x + y)^2 = x^2 + 2*x*y + y^2 := by
  ring

Details: Mathlib's tactic guide · The grind tactic

import Mathlib

-- A polynomial identity
example (x y : ℝ) :
    (x + y)^2 =
      x^2 + 2*x*y + y^2 := by
  ring

-- A statement and its proof
theorem add_zero_demo (n : ℕ) :
    n + 0 = n := by
  rfl

-- Assumptions used by the proof
#print axioms add_zero_demo

Using existing mathematics

• mathlib: definitions, theorems and tactics built by the community.
• Search instead of reproving:
  • In the editor: exact?, apply?, rw?.
  • Loogle: search by mathematical shape.
  • LeanSearch: search using natural language.
• Blueprint: a mathematical write-up linked to Lean, with a graph of dependencies.
  • Example: PFR

Details: Searching for theorems in mathlib · Lean blueprint

import Mathlib

-- A polynomial identity
example (x y : ℝ) :
    (x + y)^2 =
      x^2 + 2*x*y + y^2 := by
  ring

-- A statement and its proof
theorem add_zero_demo (n : ℕ) :
    n + 0 = n := by
  rfl

-- Assumptions used by the proof
#print axioms add_zero_demo

AI & formal proofs

• 2024: AlphaProof. Three IMO problems solved in Lean.
  • Together with AlphaGeometry 2: a silver-medal-equivalent score.
• 2025: Aristotle. Five IMO problems, a gold-medal-equivalent score.
  • Four Lean proofs and one separate geometry proof; humans formalized the statements.
• 2025: Gauss. Assisted formalization of the strong prime number theorem.
  • Includes π(x) ∼ x/log x; human blueprint and existing Lean work.
• Tools to explore: Lean Copilot, Aristotle, Leanstral (2026).

Details: AlphaProof: setup and time limits · Aristotle paper · Gauss + PNT

import Mathlib

-- A polynomial identity
example (x y : ℝ) :
    (x + y)^2 =
      x^2 + 2*x*y + y^2 := by
  ring

-- A statement and its proof
theorem add_zero_demo (n : ℕ) :
    n + 0 = n := by
  rfl

-- Assumptions used by the proof
#print axioms add_zero_demo

What does "checked" mean?

• Lean checks a precise statement, from specified definitions and assumptions.
• We must check that this statement expresses the mathematics we intended.
• sorry means "proof still missing". Lean can accept a file containing it, with a warning.
• #print axioms theorem_name shows the axioms used, including through dependencies.
  • sorryAx reveals an unfinished proof; standard logical axioms are normal.
• Trust rests on the logic and the checker. Independent checking tools add confidence.

Details: Validating a Lean proof · Comparator

import Mathlib

-- A polynomial identity
example (x y : ℝ) :
    (x + y)^2 =
      x^2 + 2*x*y + y^2 := by
  ring

-- A statement and its proof
theorem add_zero_demo (n : ℕ) :
    n + 0 = n := by
  rfl

-- Assumptions used by the proof
#print axioms add_zero_demo

Ways to run Lean

• Class sheets (open in your browser):
  • Sheet 1 · Sheet 2 · Sheet 3
• Locally: VS Code with the Lean 4 extension. Installation guide
• GitHub Codespaces: a development environment in a browser.
  • Personal accounts include a limited free allowance; usage beyond it can cost money.
• Game mode: Natural Number Game
• Use the course project: its Lean and mathlib versions belong together.

Details: Codespaces billing · Mathematics in Lean