Les mathématiques sont une base de connaissances accumulée au cours de l'histoire humaine. Chaque preuve complétée est permanente et devient disponible pour une utilisation future. La formalisation convertit les mathématiques en une base de données formelle compilée. C'est un (hyper)graphe de théorèmes, définitions et conjectures. Les arêtes codent l'implication logique et la dépendance. Les objectifs (duaux) des mathématiques sont : Expansion et Compression L'expansion ajoute de nouveaux théorèmes à la base de données, en particulier ceux qui influencent la base de données actuelle, par exemple, l'hypothèse de Riemann. La compression synthétise et refactorise la base de code, des tactiques simples pour une efficacité de base a des définitions profondes pour unifier des domaines entiers, cf. Grothendieck. L'expansion et la compression sont intrinsèques à la structure même des mathématiques.