A mathematical proof is a finite sequence of logical steps that establishes a statement with total certainty, starting from agreed-upon axioms or previously proven results, with each step following necessarily from what came before. This standard of certainty — unmatched by any other field of human inquiry — is what allows a theorem proven by Euclid over 2,000 years ago to remain exactly as true and reliable today as the moment it was first written down.
In most areas of life, "proof" means strong evidence — enough to convince a reasonable person. In mathematics, proof means something far stronger: an unbreakable logical chain, starting from starting assumptions everyone agrees on, where each individual step follows with absolute, inescapable necessity from the steps before it. If every link in that chain is genuinely solid, the conclusion is not just probably true, or true "beyond reasonable doubt" — it is true with total, permanent certainty, forever.
Checking that a mathematical pattern holds for a million specific examples, however impressive, is never itself a proof — it's merely very strong evidence (see the Goldbach Conjecture entry, verified for every even number up to 4 quintillion, yet still not proven). A genuine proof must instead show, through pure logical necessity, that the pattern must hold in every single case, including all the infinitely many cases nobody could ever individually check.
Systematic mathematical proof, in something close to its modern form, is generally traced to ancient Greek mathematics, most famously and comprehensively in Euclid's Elements (c. 300 BCE — see that entry), which built up an enormous body of geometric knowledge from just a small handful of explicitly stated starting assumptions (postulates), using pure logical deduction at every single step.
The most straightforward technique: start from known facts and axioms, and proceed step by step, using valid rules of logical inference, until the desired conclusion is reached.
Assume the opposite of what you want to prove is true, and show this assumption leads to a logical contradiction (something provably false) — since the assumption led to an impossibility, the assumption itself must have been false, meaning the original statement must be true after all. Euclid's classical proof that there are infinitely many primes (see the Prime Number entry) uses exactly this technique: assume there are only finitely many primes, then construct a new number that must have a prime factor not on the assumed complete list — a direct contradiction.
Used to prove a statement holds for every natural number: first prove it holds for the starting case (usually 0 or 1), then prove that if it holds for some arbitrary number n, it must also hold for n+1. Together, these two steps guarantee the statement holds for every natural number whatsoever, through a kind of infinite chain of falling dominoes, each one guaranteed to knock over the next.
To prove something exists, simply construct an explicit example of it. To prove some equation has a solution, exhibit a specific number that solves it.
To disprove a general claim ("all X have property Y"), it's sufficient to exhibit just a single specific X that lacks property Y — a single genuine counterexample is enough to disprove any universal claim, however much other supporting evidence might otherwise seem to favour it (see the Mertens Conjecture, tracked on the Proof Status Board, as a striking real historical example).
Every mathematical proof, when fully traced back to its logical foundations, ultimately rests on a starting set of axioms taken as given without further proof — in essentially all of modern mathematics, these are the ZFC axioms (see that entry). A proof is only ever as reliable as the axioms it's built upon, though in practice virtually all working mathematicians accept ZFC as a completely reliable and adequate foundation for ordinary mathematical work.
The proofs mathematicians actually write and publish are typically written in a mix of precise mathematical notation and ordinary natural language, relying heavily on shared context, convention, and the reader's own mathematical judgment to fill in routine or "obvious" steps. A formal proof, by contrast, is a fully explicit sequence of logical steps, each one justified by an exactly specified, mechanically checkable rule of inference, with absolutely no gaps or appeals to intuition left unstated. In principle, every ordinary mathematical proof could be translated into a fully formal one — though doing so explicitly is usually extraordinarily tedious, and mathematicians essentially never do it in full for anything beyond the simplest results.
Modern proof assistants (software such as Lean, Coq, Isabelle, and HOL Light) allow mathematicians to construct genuinely fully formal proofs with computer assistance, with every single logical step mechanically checked by the software itself, leaving no room whatsoever for human oversight or logical gaps to slip through undetected. Major results verified this way include the Four Colour Theorem (Gonthier, Coq, 2005) and the Kepler Conjecture (the Flyspeck project, HOL Light and Isabelle, 2014 — see those entries), and a large-scale, ongoing collaborative effort (led by Kevin Buzzard and others, begun 2024) is even working to formally verify Andrew Wiles's proof of Fermat's Last Theorem in Lean.
Some proofs (the original 1976 Four Colour Theorem proof, and Thomas Hales's original 1998 Kepler Conjecture proof — see those entries) are so computationally extensive that no single human being could realistically verify every step by hand within a practical timeframe. This raises genuine and still actively discussed philosophical questions about the exact nature of mathematical certainty once a proof's verification depends essentially on trusting a computer program rather than on direct, complete human comprehension of every logical step — a genuinely modern epistemological challenge that Euclid, working with entirely human-checkable geometric arguments, never had to confront.
Gödel's Incompleteness Theorems (see that entry) prove a fundamental and permanent limitation on the entire concept of formal proof itself: within any sufficiently powerful, consistent formal system, there necessarily exist true mathematical statements that can never be proven within that system at all — not due to any current lack of mathematical cleverness or effort, but as a matter of unavoidable logical necessity. This means the ideal of complete provability — the assumption, widely held before Gödel's 1931 result, that every true mathematical statement must eventually be provable given enough ingenuity — is, remarkably, itself a false belief about the fundamental nature and limits of mathematical proof.