A mathematical proof is a deductive argument that shows a mathematical statement must be true. It starts from axioms, definitions and theorems that have already been proven, and moves forward in steps. Each step follows from earlier ones by the rules of logic. Empirical evidence or inductive reasoning can only make a claim likely. A valid proof shows that the claim holds in every case covered by its hypotheses. This is why proof sits at the center of mathematics. One account describes it as a sequence of statements linked "by strict rules of logic". The same account notes that because of this, mathematicians can rely on mathematics that was done by Euclid 2300 years ago as readily as on work done today.
Origins
Mathematical activity is much older than deductive proof. Calculation and measurement were practiced in Ancient Egypt and Mesopotamia. However, many scholars locate the birth of mathematics proper in ancient Greece around the sixth century BC, when deductive proof was first introduced. Aristotle credited Thales of Miletus with recognizing the importance of not just what we know but how we know it, and finding grounds for knowledge in the deductive method. Over the next centuries, Greek mathematicians proved that some quantities are irrational and developed the method of exhaustion. Archimedes later used that method to find areas and volumes.
Around 300 BC, Euclid codified a deductive approach to geometry in his treatise, the Elements. The book sets out definitions, postulates and common notions, then derives propositions from them in order. Well-known examples are the proof of the Pythagorean theorem and the proof that there are infinitely many prime numbers. Through the centuries, Euclid's axiomatic style was held as a paradigm of rigorous argumentation, not just in mathematics, but in philosophy and the sciences as well. Other traditions also justified their results. Chinese, Indian and Islamic mathematicians gave arguments for their algorithms and identities, though often in different forms from the Greek axiomatic model.
Methods of proof
Several common patterns of argument appear across mathematics:
- Direct proof: start from the hypotheses and reach the conclusion through a chain of implications.
- Proof by contrapositive: to prove "if P then Q", show that "not Q" implies "not P".
- Proof by contradiction: assume the statement is false and derive a logical contradiction. The classic proof that √2 is irrational works this way.
- Mathematical induction: prove a statement for a first natural number, then show that if it holds for any n, it also holds for n + 1. Together these steps establish it for all natural numbers.
- Constructive and non-constructive proofs: a constructive proof produces an explicit example of the object it claims exists. A non-constructive proof shows the object must exist without producing it. Non-constructive proofs have sometimes been controversial. For example, David Hilbert proved one of his best-known results in invariant theory nonconstructively, essentially with a proof by contradiction. This was quite controversial at the time.
- Proof by exhaustion: split the problem into a finite number of cases and check each one.
- Counterexample: a single counterexample is enough to show that a general claim is false.
In practice, published proofs are written in natural language mixed with symbolic notation. They leave out routine steps that experts can fill in themselves. Whether a proof is accepted is partly a social process: other mathematicians read and check the argument through peer review and further discussion.
Rigor and foundations
In the 17th and 18th centuries, calculus grew rapidly. Its arguments about infinitesimals were often intuitive. In the 19th century, Cauchy, Weierstrass and others rebuilt analysis on precise definitions of limits and continuity. The discovery of non-Euclidean geometry also showed that axioms are best treated as assumptions, not self-evident truths.
Around 1900, mathematicians tried to put all of mathematics on a secure logical basis. Key tools were set theory, symbolic logic and axiom systems such as the Peano axioms. By the early 1900s, they settled on the axioms they wanted to use. They also introduced different logical systems and standards in an effort to further "formalize" their arguments. In this framework, a formal proof is a finite sequence of formulas, and each formula is an axiom or follows from earlier ones by a fixed inference rule. Hilbert hoped to prove that such systems are consistent. Gödel's incompleteness theorems (1931) showed that this hope had limits. Any consistent formal system strong enough to express arithmetic contains true statements it cannot prove, and it cannot prove its own consistency.
Computer-assisted proof
Computers have changed both how proofs are found and how they are checked. In 1976, the four color theorem was the first major theorem to be verified using a computer program. The four color theorem proof relied on checking a very large number of cases by machine. This raised philosophical questions. Some critics argue that proofs involve so many logical steps that they are not practically verifiable by human beings.
Another example is the Kepler conjecture on sphere packing, first stated by Johannes Kepler in 1611. Thomas Hales announced a computer-heavy proof in 1998. Referees said that they were "99% certain" of the correctness of Hales' proof. In response, Hales started the Flyspeck project to verify the proof formally. It was officially completed on Aug. 10, 2014. The project used a combination of the Isabelle and HOL Light proof assistants.
Proof assistants have been developed since the 1960s. With a proof assistant, the user writes out every definition and every step of a proof in a language the machine can read, and the software checks the logic. Widely used proof assistants include Coq, Isabelle, and Lean. Lean's community library, Mathlib, has grown quickly. By early 2026 it held more than 120,000 definitions and about a quarter of a million verified theorems. Formalization can also find errors in classic texts. A 2024 formalization of Book I of Euclid's Elements in Lean uncovered errors in Euclid's proofs.
Proof and artificial intelligence
Automated theorem proving goes back to the early days of computer science. Recent progress has come from combining it with machine learning. At the 2024 International Mathematical Olympiad, Google DeepMind's AlphaProof and AlphaGeometry 2 combined to score one point below the human gold level cutoff. AlphaProof generates proofs in the formal language Lean. The primary advantage of this formal approach is guaranteed correctness.
In 2025, systems based on large language models wrote competition proofs in natural language. Google DeepMind's Gemini Deep Think solutions were officially graded and certified at 35/42, the gold-medal standard. OpenAI reported the same score from its own evaluation, which was graded by former medalists rather than certified by IMO coordinators. Natural-language proofs from AI systems still need human checking. Their arrival has renewed interest in pairing artificial intelligence with formal verification.
References
- The History and Concept of Mathematical Proof Steven G. Krantz1math.wustl.edu
- 1. Introduction — Logic and Proof 3.18.4 documentationleanprover-community.github.io
- In Math, Rigor Is Vital. But Are Digitized Proofs Taking It Too Far?quantamagazine.org
- Computer-assisted proofen.wikipedia.org
- Kepler conjectureen.wikipedia.org
- Kepler Conjecture -- from Wolfram MathWorldmathworld.wolfram.com
- Autoformalizing Euclidean Geometryarxiv.org
- GitHub - loganrjmurphy/LeanEuclid: LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean. · GitHubgithub.com
- An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematicsarxiv.org
- Winning Gold at IMO 2025 with a Model-Agnostic ...arxiv.org
- AI Reasoning: Gold-Medal Performance at the 2025 IMOintuitionlabs.ai