La matematica è una base di conoscenza accumulata nel corso della storia umana. Ogni dimostrazione completata è permanente e diventa disponibile per un uso futuro. La formalizzazione converte la matematica in un database formale compilato. È un (iper)grafo di teoremi, definizioni e congetture. I bordi codificano l'implicazione logica e la dipendenza. Gli obiettivi (doppio) della matematica sono: Espansione e Compressione L'espansione aggiunge nuovi teoremi al database, in particolare quelli influenti sul database attuale, e.g. l'ipotesi di Riemann. La compressione sintetizza e rifattorizza il codice, da tattiche semplici per una base di efficienza di base a definizioni profonde per unificare interi domini, c.f. Grothendieck. Espansione e compressione sono intrinseche alla struttura della matematica stessa.