數學是人類歷史上積累的知識基礎。每一個完成的證明都是永久的，並且可以供未來使用。 形式化將數學轉換為一個編譯的正式數據庫。它是一個（超）圖，包含定理、定義和猜想。邊緣編碼邏輯的含義和依賴性。 數學的（雙重）目標是： 擴展與壓縮 擴展將新的定理添加到數據庫中，特別是那些對當前數據庫有影響的定理，例如：黎曼假設。 壓縮合成並重構代碼庫，從簡單的策略以提高基本效率，到深層定義以統一整個領域，參見：Grothendieck。 擴展與壓縮是數學本身結構的內在特徵。