Một lý thuyết toán học gồm những tiên đề và một hệ thống quy tắc suy luận. Chứng minh toán học là dùng các quy tắc suy luận để đi từ các tiên đề đến các định lý, phát biểu... Các định nghĩa dựa theo những định nghĩa đã có trước. Vì thế phải có những khái niệm nguyên thủy đầu tiên, không định nghĩa (không nói chúng là gì, nhưng chúng phải thỏa mãn những tiên đề của lý thuyết).
Hệ tiên đề được sử dụng rộng rãi trong toán học hiện nay là lý thuyết tập hợp ZFC. Đối tượng nguyên thủy (không định nghĩa) là các tập hợp. Một khái niệm được coi là định nghĩa rõ ràng nếu nó là một tập hợp, một phần tử của một tập hợp nào đó... Hình thức hóa về cơ bản là đưa các khái niệm về lý thuyết tập hợp, sử dụng các mệnh đề toán học (gồm các toán hạng như các số 0,1, 2,..., quan hệ giữa các toán hạng như dấu =, <, >, ..., và các toán tử của logic vị từ "và", "hoặc", "$\implies$", $\iff$,... cũng như hai lượng từ của logic bậc nhất $\forall$, $\exists$.
$$\text{H}^r_{\text{ét}}(\mathcal{O}_K, M) \times \text{Ext}^{3-r}_{\mathcal{O}_K}(M,\mathbb{G}_m) \to \text{H}^3_{\text{ét}}(\mathcal{O}_K,\mathbb{G}_m) \cong \mathbb{Q}/\mathbb{Z}.$$
"Wir müssen wissen, wir werden wissen." - David Hilbert