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