Lean formalization culture
Overview
"Mathematics in code"—Buzzard evangelized writing math in Lean; trained Tao, Commelin, and others. Created the culture that enables digital axiomatization.
Era: 2017–
Proposed at: London, UK (Imperial College)
Formal structure
Domain: Lean 4, dependent type theory
Proof = term of type Proposition
Constraints: Constructive or classical
Objective: Formalize and verify mathematical proofs