数学是人类历史上积累的知识基础。每一个完成的证明都是永久的，并且可以供未来使用。 形式化将数学转化为一个编译的形式数据库。它是一个（超）图，包含定理、定义和猜想。边缘编码了逻辑蕴含和依赖关系。 数学的（双重）目标是： 扩展与压缩 扩展将新的定理添加到数据库中，特别是那些对当前数据库有影响的定理，例如：黎曼假设。 压缩合成并重构代码库，从简单的策略以提高基本效率，到深层定义以统一整个领域，参见：格罗滕迪克。 扩展与压缩是数学本身结构的内在特征。