Toán học là một kho kiến thức tích lũy qua lịch sử nhân loại. Mỗi chứng minh hoàn thành là vĩnh viễn và trở nên có sẵn cho việc sử dụng trong tương lai. Việc hình thức hóa chuyển đổi toán học thành một cơ sở dữ liệu hình thức biên dịch. Nó là một (siêu) đồ thị của các định lý, định nghĩa và giả thuyết. Các cạnh mã hóa sự suy diễn và phụ thuộc logic. Các mục tiêu (đối ngẫu) của toán học là: Mở rộng & Nén Mở rộng thêm các định lý mới vào cơ sở dữ liệu, đặc biệt là những định lý có ảnh hưởng đến cơ sở dữ liệu hiện tại t.g. giả thuyết Riemann Nén tổng hợp và tái cấu trúc mã nguồn, từ các chiến thuật đơn giản cho hiệu suất cơ bản tới các định nghĩa sâu sắc để thống nhất toàn bộ lĩnh vực, c.f. Grothendieck Mở rộng & nén là bản chất của cấu trúc của chính toán học.