Matematika je znalostní báza nahromaděná během lidské historie. Každý dokončený důkaz je trvalý a stává se dostupným pro budoucí použití. Formalizace převádí matematiku na kompilaci formální databáze. Je to (hyper)graf vět, definic a domněnek. Hrany kódují logickou implikaci a závislost. (Dvojí) cíle matematiky jsou: Expanze a stlačení Rozšíření přidává do databáze nové věty, zejména ty, které mají vliv na současnou databázi např. Riemannova hypotéza Komprese syntetizuje a refaktoruje kódovou základnu, od jednoduchých taktik pro základní efektivitu až po hluboké definice pro sjednocení celých domén, srov. Grothendieck Expanze a komprese jsou nedílnou součástí samotné struktury matematiky.