What is a computer-assisted proof?
- Series
- Explain
- Summary
- A beginner-first guide to computer-assisted proof: how finite computation can become part of a rigorous argument through exhaustive reduction, interval arithmetic, controlled truncation, certificates, independent verification and formal proof assistants.
- Math Level
- GENERAL
- Index Excerpt
- A large calculation is not automatically a proof. What matters is the mathematically justified chain connecting finite computation to an exact claim, with every error relevant to the conclusion brought under control.
A computer can perform millions, billions or trillions of calculations far more quickly than a human being.
That does not normally turn those calculations into a proof.
So what has to change before mathematics is entitled to say that a computer has actually proved something?
It is a surprisingly deep question.
If a program checks a million examples and every one works, we have strong evidence.
If it checks a trillion examples, we have even stronger evidence.
But as we saw in If the Riemann Hypothesis has worked so far, why do we still need a proof?, an enormous finite collection of successful examples is still a finite collection.
A proof has to do something different.
It has to show that failure is mathematically impossible under the stated assumptions.
A computer-assisted proof does not lower that standard.
It changes how some of the work needed to meet the standard is performed.
A calculation is not automatically a proof
Imagine that we have a complicated function and want to know whether it always stays above zero.
One obvious approach would be to evaluate it at many points.
Suppose a computer checks a million of them.
Every value is positive.
We check ten million.
Still positive.
We increase the numerical precision and repeat the calculation.
Still positive.
The result may now be extremely persuasive.
But an awkward question remains.
What happened between the points we checked?
Perhaps the function dips below zero in a very narrow region between two samples.
Perhaps the calculation is approaching an infinite object by cutting it off after finitely many terms, and the neglected tail changes the answer.
Perhaps two large quantities almost cancel and the apparently small positive result is actually smaller than the accumulated rounding error.
Perhaps the finite matrix in the computer is only an approximation to an infinite-dimensional mathematical object.
Perhaps the program is evaluating exactly what we asked it to evaluate, but what we asked it to evaluate is not quite the quantity appearing in the theorem.
These are not reasons to distrust computation.
They are reasons to be precise about what a computation has established.
Numerical evidence asks:
What appears to happen in the cases we computed?
Proof asks a stronger question:
Why can the forbidden thing not happen at all?
The computer has to enter the argument
The decisive step occurs when the computation is no longer merely evidence \about\ the proof.
It becomes one of the justified steps \inside\ the proof.
A mathematical argument might show, for example, that an infinite problem can be reduced to a finite collection of cases.
The computer then checks every case.
Or an argument might reduce a theorem to establishing a numerical inequality.
The computer calculates a bound, while additional mathematics rigorously controls the rounding, approximation and omitted remainder.
Or the whole argument might be expressed in a formal language and checked step by step by a proof assistant.
The details vary enormously.
The common structure is this:
A flow from an exact mathematical claim through a justified finite reduction and certified computation to a proved conclusion. An unconnected numerical experiment sits outside the proof path.
The important arrows are mathematical.
The computer may do the heavy lifting in the middle, but the argument must establish that what the computer has checked is enough to imply the conclusion we actually care about.
(The size of the calculation is not what turns it into a proof. The crucial point is that a mathematically justified chain connects the finite computation to the exact claim.)
There is more than one kind of computer-assisted proof
The phrase \computer-assisted proof\ covers several rather different styles of mathematics.
They overlap, but it is useful to separate them.
One approach is exhaustive finite checking.
Mathematics first proves that only finitely many possibilities need to be considered. The number of possibilities may still be far too large or tedious for human beings to inspect reliably, so a computer checks them.
The famous Four Colour Theorem became an early landmark of this kind. In 1976 Kenneth Appel and Wolfgang Haken reduced the problem to a finite collection of configurations whose required properties were checked with substantial computer assistance. The result became one of the first major theorems whose accepted proof depended essentially on computer calculation. (\AMS\)
Another approach is rigorous numerical analysis.
Here the computer may calculate approximations, eigenvalues, integrals, solutions of equations or lower and upper bounds. But instead of treating ordinary floating-point answers as exact, the proof keeps track of enough error information to establish a rigorous mathematical inequality.
Interval arithmetic is one important tool for doing this. Rather than representing a quantity by one approximate number, the computation carries an interval guaranteed to contain the exact value. Carefully performed interval operations can therefore propagate rigorous enclosures through a calculation. This technique has been used in computer-assisted mathematical proofs, including work associated with the Kepler sphere-packing problem. (\SIAM\)
A third approach uses formal proof assistants.
Instead of asking a conventional numerical program to calculate some part of the argument, mathematicians encode definitions, statements and logical steps in a formal system. A comparatively small trusted proof-checking core then verifies that the conclusion follows according to the rules of the system.
The Four Colour Theorem was later given a fully computer-checked formal proof in Coq by Georges Gonthier and collaborators. (\Microsoft Research\)
Thomas Hales's proof of the Kepler conjecture provides another striking example. After the original computer-assisted proof raised questions about the practical difficulty of checking its many computational components, the Flyspeck project undertook a formal verification using the HOL Light and Isabelle proof assistants. The completed formal proof was published in 2017\. (\Cambridge University Press\)
These are all forms of computer-assisted mathematics.
But they place the computer in different parts of the logical machinery.
High precision is not the same thing as rigour
This distinction is particularly important.
Suppose a calculation gives
That number is positive.
If the calculation is reliable to twenty decimal places, perhaps we feel very confident about the sign.
But confidence is not yet a certified lower bound.
A computer normally represents most real numbers approximately. Intermediate operations are rounded. Repeated operations can accumulate error. Subtracting two nearly equal large numbers can lose meaningful digits. An infinite process may have been truncated. A continuous object may have been represented by a finite grid or matrix.
Using high-precision arithmetic can make these problems much smaller.
It does not automatically make them disappear.
A hundred-digit approximation is still an approximation.
The right question is not merely:
How many digits did we calculate?
It is:
What is the largest possible error in the quantity on which the theorem depends?
Suppose, in an entirely invented example, a rigorous calculation establishes that an exact quantity lies in the interval
(The computer is not claiming that the exact answer is one particular decimal. It is claiming that the exact answer is guaranteed to lie somewhere inside this whole interval.)
Now we know something stronger than a long decimal approximation.
The entire certified interval lies above zero.
Therefore
That final statement is exact.
The computation involved approximations, but the proof controls them tightly enough that the exact mathematical conclusion survives.
That is the basic idea behind interval certification.
The missing tail can matter
Infinite mathematical objects create another common difficulty.
Computers are finite machines.
They cannot literally add infinitely many terms, integrate over infinitely many independent pieces or store an infinite-dimensional matrix.
So an infinite object often has to be split into a finite part that the computer can handle and a remainder that mathematics can bound.
Suppose an exact quantity has the form
Here is the finite part that we calculate and is everything left over.
This kind of finite replacement is a form of tail truncation.
Now suppose rigorous computation gives
while a separate mathematical estimate proves
Then even in the worst possible direction,
(The omitted infinite tail is allowed to behave as badly as the proved error bound permits. Even then, it is not large enough to push the exact quantity through zero.)
Notice what happened.
The computer never calculated the infinite object.
It did not need to.
Mathematics established that a finite calculation plus a rigorous bound on everything omitted was sufficient to settle the exact question.
This pattern appears again and again in rigorous computational mathematics.
The art is often not in making the computer calculate a larger finite approximation.
It is in proving that the gap between the finite approximation and the exact mathematical object is small enough to control.
A positive-looking answer may still prove nothing
This is why numerical stability is useful but is not itself proof.
Suppose a result hardly changes when we double the precision.
Then hardly changes when we double it again.
Then survives a larger matrix.
Then survives a finer grid.
Then survives a different algorithm.
That is excellent evidence.
It tells us that the observed phenomenon probably is not a fragile numerical accident.
But unless we have a theorem explaining what the finite computation says about the exact mathematical object, there can still be a logical gap.
The calculation may be wonderfully stable on every finite approximation we have tried while the limiting object remains uncontrolled.
Computer-assisted proof is what closes that gap.
What is a certificate?
The word \certificate\ appears frequently in computational mathematics.
It does not always mean exactly the same thing.
Broadly, a certificate is finite evidence produced or checked by a computation which, together with the surrounding mathematics, is sufficient to establish the claimed result.
Sometimes the certificate is a list of finitely many cases and the outcome of checking each one.
Sometimes it consists of exact rational data.
Sometimes it contains interval bounds.
Sometimes it is a collection of inequalities.
Sometimes a large and complicated program produces a relatively small object that can be checked independently by a much simpler program.
And in a formal proof assistant, the analogue may be a formal proof object whose correctness is checked by a small logical kernel.
This leads to a useful design principle.
The less of the argument we have to trust blindly, the better.
A complicated program that prints
\TRUE\
is not a particularly satisfying mathematical certificate.
A system in which a complicated program produces detailed evidence that can be checked by a smaller, simpler and independently understandable verifier is much stronger.
The computation becomes something that can itself be interrogated.
But what if the program has a bug?
This objection cannot simply be waved away.
Programs can contain bugs.
Compilers can contain bugs.
Libraries can contain bugs.
Hardware can fail.
Formalisation can encode the wrong theorem.
A beautifully verified computation can rigorously prove a statement that turns out not to be the statement the mathematicians thought they had formalised.
Computer assistance does not remove the problem of trust.
It lets us reorganise it.
Different proof architectures reduce different risks.
Exact arithmetic can eliminate rounding uncertainty.
Interval arithmetic can enclose it.
A small independent checker can reduce dependence on a complicated primary program.
Running the calculation at different precisions can expose instability.
A genuinely independent reproduction can catch assumptions or software errors shared by one implementation.
Formal proof assistants can reduce a huge logical argument to a much smaller trusted kernel.
Human mathematical review checks whether the formal or computational problem really corresponds to the intended theorem.
None of these is magic.
Together they can create a much stronger evidential chain.
Repeating a calculation is not the same as independently verifying it
Suppose I run a program today and obtain a result.
Tomorrow I run the same program again.
I obtain the same result.
That tells me something useful.
The computation is reproducible under those conditions.
But if the program contains the same mistake on both days, I will reproduce the mistake perfectly.
Even running the same source code on another computer does not eliminate errors in the underlying algorithm.
Independent verification becomes stronger when some of the assumptions change.
A second implementation written separately may catch a coding error.
A different numerical method may expose a hidden instability.
An independent derivation may detect that the original finite reduction was wrong.
A small certificate checker may test the output without repeating the complicated path that produced it.
Formalisation may reveal an assumption that ordinary prose had left implicit.
This is why verification has layers.
No single one of them should be mistaken for all the others.
Is a formal proof better than a computer-assisted proof?
This question contains a hidden category mistake.
A formal machine-checked proof is itself a kind of computer-assisted proof.
But not every computer-assisted proof is fully formalised.
A rigorous numerical proof may contain human-written mathematical arguments together with certified calculations.
An exhaustive proof may rely on a theorem reducing an infinite class to finitely many cases and a program checking those cases.
A formal proof assistant attempts to encode much more of the logical chain in a language whose deductions can be mechanically checked.
Formalisation can provide extraordinary assurance.
It can also require enormous effort.
The Flyspeck project is a good illustration: converting the Kepler sphere-packing proof into a formally checked object became a substantial mathematical and engineering project in its own right. (\Cambridge University Press\)
So “computer-assisted” does not describe one fixed proof standard.
It describes a family of methods in which computation carries proof-critical work.
The important question is always more specific:
What exactly was calculated?
What mathematical reduction made that calculation sufficient?
Which approximation errors were controlled?
What part of the system has to be trusted?
What can another researcher independently check?
And what precise theorem follows?
What changes when AI is involved?
Artificial intelligence introduces another source of possible confusion.
An AI system can suggest a conjecture.
It can search for patterns.
It can propose a proof strategy.
It can write computer code.
It can discover a useful representation.
It can produce algebra.
It can even generate candidate formal proofs.
None of those activities lowers the standard for proof.
If an AI produces a piece of code which prints a desirable answer, the answer does not become a theorem because the code was generated by an unusually capable system.
If an AI generates a valid formal proof which a trusted proof assistant checks, the mathematical status comes from the checked proof.
If it designs a rigorous numerical certificate whose bounds are independently validated, the status comes from the certificate and the mathematics connecting it to the theorem.
The origin of an argument and the validity of an argument are different questions.
This matters increasingly as mathematical research becomes more computational.
AI may change how candidate ideas are discovered.
It does not change what the word \proof\ has to mean.
So when does the calculation actually become a proof?
There is no single mechanical recipe that covers every branch of mathematics.
But a useful dividing line is this.
A computation becomes proof-critical when the argument establishes all the way from the exact mathematical assumptions to the exact mathematical conclusion that the finite machine calculation is sufficient.
If the calculation contains approximation, the approximation has to be controlled.
If an infinite object is truncated, the remainder has to be bounded.
If a continuous domain is broken into finitely many pieces, the reduction has to cover the entire domain.
If finitely many cases are checked, mathematics has to establish that the list really is exhaustive.
If floating-point arithmetic is used in a sign-sensitive argument, rounding uncertainty has to be accounted for.
If software output acts as a certificate, there must be a reason that accepting that certificate implies the theorem.
The proof is therefore not:
the computer says yes.
It is:
mathematics shows that this precisely specified computational task is sufficient; the task has been carried out with the required guarantees; therefore the mathematical conclusion follows.
That difference is the whole subject.
Where Riemann Console enters the story
This distinction recently became directly relevant to the public Riemann Console record.
A September 2026 milestone, A route-critical obstruction has been closed in the Riemann Hypothesis programme, describes a situation in which exploratory computation had produced strong evidence for a required positivity statement.
That evidence was not treated as proof.
The decisive margin was small enough that ordinary floating-point calculation, plotting and naive finite truncation were not considered sufficient. Several attempts to certify the result failed before the project obtained a rigorous positive lower bound with the relevant numerical and truncation errors controlled. The public milestone therefore records a change from numerical evidence and conditional use to an internal computer-assisted theorem-level result. It also explicitly states that the Riemann Hypothesis remains unproved and that the result has not undergone independent external mathematical review.
The exact private proof architecture is deliberately not part of this Explain article.
What matters here is the general distinction.
The project did not decide that the computation had become a proof because the numbers looked convincing.
It changed the status of the result only when the finite computation and the uncertainty surrounding that computation had been brought inside a mathematical argument strong enough to imply the required conclusion.
That is precisely what computer-assisted proof is for.
Computers do not weaken proof
There is sometimes a temptation to imagine two opposing traditions.
On one side sits pure human mathematics: elegant, conceptual and rigorous.
On the other sits computation: enormous, mechanical and somehow less mathematical.
Real mathematical practice is much less tidy.
Human proofs contain bookkeeping.
Computer-assisted proofs contain ideas.
A proof which reduces an infinite problem to a finite computation may require remarkable conceptual insight before the computer ever runs.
A rigorous numerical estimate may depend on delicate analysis to explain why a finite enclosure controls an infinite object.
Formalisation can expose hidden assumptions and force mathematicians to understand definitions with unusual precision.
And a computer may spend hours performing the least conceptually interesting part of an argument because that happens to be the part human beings are worst equipped to execute reliably.
The standard has not changed.
The theorem must still follow.
What has changed is the range of mathematical labour that can participate in establishing that fact.
The one sentence to remember
A computer-assisted proof is not a calculation so large or so precise that we decide to trust it.
It is a mathematical argument in which the computation, the connection between the finite calculation and the exact problem, and every uncertainty relevant to the conclusion are themselves brought under control.