Digital axiomatization of mathematics
Overview
Program to axiomatize all of mathematics digitally and verify with AI. Tao leads the effort; coordinates formalization projects across number theory, analysis, combinatorics.
Era: 2010s–
Proposed at: Los Angeles, USA (UCLA)
Formal structure
Domain: Lean 4, Mathlib, formal proofs
Theorem → formal proof → machine-verified
Constraints: ZFC or type-theoretic foundations
Objective: All mathematics derivable and verifiable