A matemática é uma base de conhecimento acumulada ao longo da história humana. Cada prova concluída é permanente e torna-se disponível para uso futuro. A formalização converte a matemática em uma base de dados formal compilada. É um (hiper)grafo de teoremas, definições e conjecturas. As arestas codificam implicação lógica e dependência. Os objetivos (duais) da matemática são: Expansão e Compressão A expansão adiciona novos teoremas à base de dados, particularmente aqueles influentes na base de dados atual e.g. a hipótese de Riemann A compressão sintetiza e refatora a base de código, desde táticas simples para eficiência básica a definições profundas para unificar domínios inteiros, c.f. Grothendieck Expansão e compressão são intrínsecas à estrutura da própria matemática.