Las matemáticas son una base de conocimiento acumulada a lo largo de la historia humana. Cada prueba completada es permanente y estará disponible para su uso futuro. La formalización convierte las matemáticas en una base de datos formal compiladora. Es un (hiper)grafo de teoremas, definiciones y conjeturas. Las aristas codifican implicación y dependencia lógica. Los objetivos (duales) de las matemáticas son: Expansión y compresión La expansión añade nuevos teoremas a la base de datos, especialmente aquellos influyentes en la base de datos actual por ejemplo, la hipótesis de Riemann La compresión sintetiza y refactoriza la base de código, desde tácticas simples para la eficiencia básica a definiciones profundas para unificar dominios enteros, cf. Grothendieck La expansión y la compresión son intrínsecas a la estructura de las matemáticas mismas.