Математика — це база знань, накопичена протягом історії людства. Кожен заповнений доказ є постійним і стає доступним для подальшого використання. Формалізація перетворює математику на компіляційну формальну базу даних. Це (гіпер)граф теорем, визначень і гіпотез. Ребра кодують логічну імплікацію та залежність. (Подвійні) цілі математики такі: Розширення та стиснення Розширення додає нові теореми до бази даних, особливо ті, що впливають на поточну базу даних наприклад, гіпотеза Рімана Стиснення синтезує та рефакторить кодову базу, починаючи з простих тактик для базової ефективності до глибоких визначень для об'єднання цілих доменів, див. Гротендік Розклад і стиснення є невід'ємною частиною самої структури математики.