# Proof

**Type:** Concept  
**Domain:** Foundations & Logic  
**Codex URL:** /mathematics/foundations-logic/proof/  
**Entry status:** Live — v1.0 (2026-05-27)

## Summary
A finite sequence of logical steps establishing a statement with total certainty.

## Proof techniques
- **Direct proof:** step by step from axioms to conclusion
- **Contradiction:** assume the opposite, derive an impossibility (e.g. Euclid's infinitude of primes)
- **Induction:** prove base case + "n implies n+1" for all naturals
- **Construction:** exhibit an explicit example
- **Counterexample:** disprove a universal claim with a single exception (see Mertens Conjecture)

## Foundation
Every proof ultimately rests on axioms taken as given — in modern mathematics, ZFC (see that entry).

## Formal vs ordinary proof
Ordinary proofs mix notation and natural language; formal proofs are fully explicit, mechanically checkable step sequences.

## Computer-verified proofs
Proof assistants (Lean, Coq, Isabelle, HOL Light) mechanically check every step. Examples: Four Colour Theorem (Gonthier, Coq, 2005), Kepler Conjecture (Flyspeck, 2014). Fermat's Last Theorem formalization in Lean ongoing (Buzzard, begun 2024).

## Proofs too long to hand-check
Four Colour Theorem (1976) and original Kepler proof (1998) — raised genuine philosophical questions about mathematical certainty via computer trust.

## Gödel's limitation
Incompleteness theorems prove some true statements can never be proven within any sufficiently powerful consistent system — a fundamental limit on provability itself.

## Sources
### Tier 1
- Velleman, D.J. (2019). How to Prove It. 3rd ed.
- Heath, T.L. (1956). Euclid: The Thirteen Books of the Elements.
### Tier 2
- Avigad, J. (2021). Mathematical logic and computation.

---
*Mathematics Codex entry v1.0 — added 2026-05-27 — thecodex.expert/mathematics/*