Formalising mathematics - an introduction

formal-verificationproof-assistantsleanmathematics

Abstraction: Kevin Buzzard on Lean proof assistant and digitizing mathematics

Key points:

Kevin Buzzard (Imperial College) switched from algebraic number theory to formal mathematics after concluding the peer-review system doesn't scale — papers with contradictory results have both appeared in the Annals of Mathematics with no erratum
Lean (the proof assistant) can now handle serious modern research mathematics; a team of 20 researchers formalized the Feit-Thompson theorem (400-page proof) over six years using Coq/Gonthier
Digitizing mathematics is analogous to the vinyl-to-digital transition: the crucial shift is not the medium but the new ways the content can be used — AI, interactive textbooks, automated checking
Current ML/AI theorem-proving is bottlenecked by lack of quality mathematical databases; existing formal libraries have structural issues that make them poor training data for AI
Formalisation eliminates edge-case errors in teaching materials and enables interactive problem sheets where answers can be automatically verified
Other proof systems mentioned: Coq, Isabelle, Metamath, Mizar, Agda, HOL 4, HOL Light

Connections: Kevin Buzzard · Lean Prover · Formal Verification · Proof Assistants · Formalized Mathematics