A proof is a rigorous mathematical argument that unequivocally demonstrates the truth of a given proposition. A mathematical statement
that has been proven is called a theorem.
According to Hardy (1999, pp. 15-16), "all physicists, and a good many quite respectable mathematicians, are contemptuous about proof. I have heard Professor Eddington, for example, maintain that proof, as pure mathematicians understand it, is really quite uninteresting and unimportant, and that no one who is really certain that he has found something good should waste his time looking for proof.... [This opinion], with which I am sure that almost all physicists agree at the bottom of their hearts, is one to which a mathematician ought to have some reply."
To prove Hardy's assertion, Feynman is reported to have commented, "A great deal more is known than has been proved" (Derbyshire 2004, p. 291).
A computer-assisted proof can reduce a proposition to finitely many cases and use a program to check each case. Appel and Haken's proof
of the four-color theorem used computer computations for checks that were impractical to carry
out by hand (Gonthier 2008).
A proof assistant checks a formal derivation, including the argument that connects any verified computations to the conclusion. Gonthier (2008) describes a later formal
proof of the four-color theorem checked by
Coq, covering both the logical argument and its computational steps.
In AI-assisted mathematics, a model can propose a formal derivation and a proof assistant such as Lean can check it against
a precisely stated proposition (de Moura and Ullrich
2021).
Machine checking separates two questions. It can verify that a formal derivation establishes a formal statement from a stated axiomatic
system, but this does not itself show that the formal statement faithfully expresses
the intended informal claim. Checking the formalization is therefore distinct from
checking the derivation (Wolfram 2026).
A proof can establish a result without explaining why its key ideas work or how they might apply elsewhere. In discussing AI-generated proofs, Terence Tao observed that producing more proofs need not yield more mathematical understanding (Numberphile 2026).
A page of proof-related humor is maintained by Chalmers.
