数学は人類の歴史を通じて蓄積された知識の基盤です。完成した各証明は永久的であり、将来の利用可能となります。 形式化は数学をコンパイルする形式データベースに変換します。これは定理、定義、予想の(ハイパー)グラフです。エッジは論理的含意と依存性を符号化します。 数学の(二重の)目的は以下の通りです: 膨張と圧縮 拡張は特に現在のデータベースに影響を与える定理をデータベースに追加します 例えばリーマン仮説 圧縮は基本的な効率のための単純な手法からコードベースを合成し、リファクタリングします さらに、ドメイン全体を統一するための深い定義、 参照:グロタンディーク 展開と圧縮は数学そのものの構造に本質的に組み込まれています。