Skip to content

What is this about

Formal verification (of mathematical theorems) - Process to verify a proof of mathematical statement using computer. - Related: software verification. (not the focus of this class) - "Translation: mathematics \(\leftrightarrow\) logic \(\leftrightarrow\) computer science "

Some historical successes -- 4CT

  • 4-color theorem: every planar graph is 4-colorable
    • 1976 Appel&Haken -- first proof using computer (still a lot of human case-checking)
    • 1997 Robertson, Sanders, Seymour and Thomas -- still using computer, correcting mistakes in the case-checking
    • 2005 Werner&Gonthier -- formal proof (in Coq)

Some historical successes -- Kepler's conjecture

  • Kepler's conjecture: best packing of equal balls
    • In1990, Wu-Yi Hsiang claimed a proof -- not accepted
    • In 1998, Hales announced a proof (250 pages + 3 GB of data)
    • In 2003, a panel of 12 experts "99% certain" of the correctness of the proof, but they could not certify the correctness of all of the computer calculations.

WIP: Fermat's last theorem:

\(x^n + y^n = z^n\) has no solution in positive integers with \(n > 2\).

ATP vs ITP

Automated vs interactive theorem provers.

List of alternative ITPs

Name Initial release
Mizar 1973
Isabelle 1986
Coq \(\to\) Rocq 1989
LEAN 2013

Levels of help & automation

  • write formal proof -- sequence of formulas, etc.
  • write program that constructs formal proof -- tactics -- more human-like
  • use existing theorems -- mathlib
  • tools to search in mathlib
  • blueprint -- way to create and visualize structure of large proof Example from Terry Tao -- PFR
  • Lean Copilot --- getting help from LLMs
  • Project Gauss
    • Recently formalized the proof of Prime number theorem: number of primes among \(1, \dots, n\) is \((1+o(1)) \frac{n}{\ln n}\)
    • Produced ~25,000 lines of Lean code, comprising over 1,000 theorems and definitions.

Ways how to run LEAN

  • https://live.lean-lang.org/
  • Github codespaces (needs to pay?)
  • locally -- VS code with Lean4 extension
  • "game mode" -- https://adam.math.hhu.de/#/g/leanprover-community/NNG4