Matematica este o bază de cunoștințe acumulată de-a lungul istoriei umane. Fiecare dovadă completată este permanentă și devine disponibilă pentru utilizare viitoare. Formalizarea transformă matematica într-o bază de date formală compilare. Este un (hiper)graf de teoreme, definiții și presupuneri. Muchiile codifică implicația și dependența logică. Obiectivele (duale) ale matematicii sunt: Expansiune și compresie Extinderea adaugă noi teoreme bazei de date, în special cele influente pentru baza de date actuală de exemplu, ipoteza Riemann Compresia sintetizează și refactorizează baza de cod, pornind de la tactici simple pentru eficiență de bază la definiții profunde pentru a unifica domenii întregi, c.f. Grothendieck Expansiunea și compresia sunt intrinseci structurii matematicii în sine.