Математика — это база знаний, накопленная за историю человечества. Каждое завершенное доказательство является постоянным и становится доступным для будущего использования. Формализация преобразует математику в компилируемую формальную базу данных. Это (гипер)граф теорем, определений и гипотез. Ребра кодируют логическое следствие и зависимость. (Двойные) цели математики: Расширение и Сжатие Расширение добавляет новые теоремы в базу данных, особенно те, которые влияют на текущую базу данных, например, гипотеза Римана. Сжатие синтезирует и рефакторит кодовую базу, от простых тактик для базовой эффективности до глубоких определений, чтобы объединить целые области, сравнительно с Гротендиком. Расширение и сжатие являются неотъемлемыми частями структуры самой математики.