Matematiikka on ihmiskunnan historian aikana kertynyt tietopohja. Jokainen valmis todiste on pysyvä ja tulee saataville myöhempää käyttöä varten. Formalisointi muuntaa matematiikan muodolliseksi tietokannaksi. Se on (hyper)graafi lauseista, määritelmistä ja konjektuureista. Reunat koodaavat loogisen implikaation ja riippuvuuden. Matematiikan (kaksi) tavoitteet ovat: Laajennus ja pakkaus Laajennus lisää tietokantaan uusia teoreemoja, erityisesti niitä, jotka vaikuttavat nykyiseen tietokantaan esim. Riemannin hypoteesi Pakkaus synteesi ja refaktoroi koodipohjan, yksinkertaisista taktiikoista perustehokkuuteen syviin määritelmiin, jotka yhdistävät kokonaisia alueita, vrt. Grothendieck Laajennus ja puristus ovat matematiikan rakenteen olennaisia.