How the work is done — drawing problems, and the discipline of checking
Computation aimed at unsolved problems leans toward seeing what it wants to see. With a problem whose answer nobody knows, there is nothing outside to tell you when you are wrong. This page collects the rules that hold that lean in check by procedure. Draw problems at random, and move on when stuck. Write the prediction before measuring, and observe only after the controls and the calibration have passed. Claims that cannot be closed by machine checking are not put forward.
Draw problems at random
Choose the problems yourself, and a bias enters at the moment of choosing. What remains are the problems where the tools at hand look likely to work, problems touched before, problems that look likely to yield a result. That bias cannot be seen from the side of the results — the impression that "this method works on this kind of problem" may be nothing but a product of how the problems were chosen, and there is no telling the difference.
Make a list of problems and draw from it with random numbers, and the bias is cut at the stage of selection. Even when a drawn problem is out of reach, that is information about the distribution of problems. Line up where each problem stops, and quite different problems sometimes turn out to have the same shape — for instance, "the part that a finite check can settle is already closed, and all that remains is the part that this method cannot reach in principle". Digging at one problem alone, this shape cannot be seen.
The order of the draws, and the intervals at which problems were changed, are kept as measurements taken from the computer's clock. Felt time is remembered as long while stuck and short while moving. A record of what was done can be more accurate than the introspection of the one who did it, so the intervals are read from the record, not from memory.
The record of the first round drawn this way is in Drawing unsolved problems at random.
When stuck, move to another problem
Most of being stuck comes from the view having fixed on one angle. Keep holding the same tool in front of the same problem, and the view does not move. Move to another problem, and the tools used there, or the shapes found there, sometimes work from the side when you come back to the first. A test built for one problem passing straight through on the neighbouring problem is something that actually happens.
When moving on, the thinking at the point of being stuck is written down — what was tried, where it stopped, and why it was thought to have stopped. A discarded hypothesis is kept together with the reason it was discarded. A "it didn't work" without a reason does nothing to stop the next attempt from walking into the same road.
Moving on has a price too. It easily leads to a state where every problem has been gone into only once, to a single depth. So it becomes a back and forth: if another shape shows itself where you moved to, go back; if nothing shows, go on to the next.
The outlook that "given enough computing resources, it could go further" does not count as getting past being stuck. Computation is valuable for seeing tendencies and getting ideas, but what should be headed for first is the part where it is not known how to proceed.
The discipline of checking
With a problem whose answer is not known, nobody notices when the check itself is wrong. When a number comes out as expected, it is hard to tell, after the fact, whether that is a property of the object or a property of how the check was built. So the means of telling them apart is put in place before the observation. Every one of the rules below exists for this single point.
1. Write the prediction before the observation (pre-registration)
Before running a computation, write down what you expect to come out, and which values would count as the hypothesis having failed. Decide the criterion after seeing the result, and the criterion moves to fit the result. Whether the prediction held is reported alongside the result, and failed predictions are not erased.
For the same reason, a computation's output is not allowed to print a sentence stating the conclusion ahead of the numbers. The reader's eye is drawn to the sentence and stops checking the numbers. Numbers are written after running; reasons are written after checking.
2. Pass a positive control and a negative control
A check that answers "none" or "0 found" may, on its own, be saying nothing at all — a check built so that it cannot detect anything also answers "0 found". So before the real run, the same check is used to confirm that what should be there comes out (positive control) and that what should not be there does not come out (negative control). Only the "0 found" of a check that has passed both means 0.
3. Calibrate alone, before the real run
After transcribing a general formula from the literature into your own setting, and before starting the real computation, check your formula against a special case for which the literature gives concrete values. Calibrate at the same time as the real run, and a discrepancy cannot be separated into an error in transcribing the formula and a property of the object. The values used for calibration are taken from primary sources or from identities, never written from memory.
4. Measure and judge with separate implementations
Compute both sides of an identity with the same components, and an error in a component enters both sides in the same form, and the difference vanishes at 10−12. The agreement shows nothing about correctness. The implementation that measures and the one that judges are kept separate, and at least one independent route — another program, another numerical method, another representation such as the position side and the momentum side — is used to confirm.
5. Establish detection power on synthetic data before observing
When a statistical regularity turns up in the object, first test whether the same regularity also appears in synthetic data that does not use the structure of the object. If it does, it is not a property of the object but an identity coming from how the statistic was built. Conversely, before looking at the real data, embed the effect you are looking for in synthetic data and measure whether the check picks it up — its detection power. To say "it was not seen" with a check that cannot pick it up is to say nothing.
Example: 1/12 appeared in a certain statistic taken over the zeros of the Riemann zeta function, but the same value came out on a sequence of points unrelated to zeta. It was an identity. The article The Riemann hypothesis sets this test down in one sentence: "if structure shows up in a statistic over the zeros, first check whether the same value comes out of a point process that does not use ζ".
6. For "pick the best" procedures, subtract a floor at true value 0
Choose the best of many candidates, and the chosen value comes out positive even when there is no true effect at all. The act of choosing itself pushes the value up. So the same selection procedure is run on data where the true effect is known to be 0, and that value is subtracted as the floor. Only what rises above the floor is a candidate for an effect.
7. At least 30 samples
A quantity that varies is not read off a handful of points. With a handful, a tendency and chance cannot be told apart. For any quantity being compared, at least 30 samples are taken.
8. Do not trust numbers from an earlier computation — measure them again
A number produced by an earlier computation has meaning only together with that computation's assumptions. Carry over the number without remembering the assumptions, and a number that has lost its conditions enters the next computation as an unconditional fact. Numbers are measured again at the time they are used.
9. Check the formula as written, in the form it is written
Even when the computation that produced a formula is correct, the displayed formula copied onto the page can be wrong. What goes out is the displayed formula, so the check is done on the displayed formula. A formula that is not displayed has not been verified.
10. Do not drop conditions in a summary
Even if the body says "under this assumption", once that phrase drops out of a one-line summary, the reader sees an unconditional claim. In a summary, a line of a table, or any place where a theorem name is given, the assumptions of the claim are put on the same line. Write only the theorem name, and it is read as saying things the theorem does not say.
Claims that machine checking cannot close are not put forward
Even after passing all of the discipline above, an argument on paper can still contain things overlooked. Long case analyses and large finite checks in particular are more than even their author can fully reread. So the bar for a mathematical claim that is put forward is that it be closed in a system where a machine checks the proof (here, Lean 4 and mathlib). What cannot be closed is not made a claim that is put forward.
There is one criterion for "closed". Run #print axioms on the main theorem, and every line of the output is a subset of the three standard axioms (propext, Classical.choice, Quot.sound). It contains neither an unproved hole (sorryAx) nor the shortcut that hands computation to something outside the kernel (native_decide). The Lean label is given only to what has its axiom output recorded in the ledger.
Other claims are told apart by labels, according to how far they have been checked.
| Label | Meaning |
|---|---|
| Lean | Machine-checked. Meets the criterion above; the theorem name is given |
| paper | A proof exists, but machine checking is not done. Whenever the word "theorem" is used, this label goes with it |
| computation | The range checked on this machine, by exhaustive enumeration, interval arithmetic and the like. Not made a claim that is put forward |
| known | A known theorem, a restatement, or a confirmation of outside literature. Not new mathematics |
What machine checking does not guarantee
What machine checking guarantees is only that the conclusion follows from the proposition as written. There are three things it does not guarantee. (1) Whether the proposition manages to state what was intended — whether a definition really says what it is meant to say can only be judged by a person reading it. (2) Whether the proposition is new in the world — that is a question of the literature, and the machine says nothing about it. (3) Whether the interpretation of the values being compared against is right — whether a number in the literature is truncated or rounded, and which object it is a value for. So even for claims carrying the Lean label, the definitions are shown in a readable form, and what is being compared against is written with its source.
Which label each claim carries is in The ledger of claims; the machine-checking bundle and how to check it are in The Lean verification bundle.
The bar for calling something "new"
Only what has been carried through to a final proof is called "new". Intermediate views, and regularities seen in computation, are written in the form "whether this is new is not known, but mathematically there is a fact like this". It is a way of writing that stands on the assumption that researchers in the field may already know it.
Even for what has been carried through to a proof, the most that can be written is "no statement of the same form was found in the literature searched". The range searched — which literature, which databases, which search terms — is stated alongside. This is so that the reader can see that nothing is being said about what lies outside that range.
Finding an earlier record does not stop the work there. Even when the value came out first elsewhere, meaning can remain as a proof by another route, a machine check, or a by-product of a classification. In that case the position is written accurately, and no priority is claimed. Not being able to obtain the original paper is not a reason to stop either. One line saying "this may be known" is written, and the statement and proof go ahead.
Typos in outside sources are not something to report
Finding a typo or a numerical discrepancy on an outside site or in a paper is not held up as a result. Other readers have likely noticed it too, and sometimes it has been left in on purpose. Lining up remarks that have little to do with the mathematical content pulls the article's centre of gravity away from the mathematics.
Only when it bears directly on the computation in the text — when a value taken from a source differs and that changes a comparison made here — is the value used written down together with its source. It is written not as a correction, but as making explicit an assumption of the computation here.
Related: Drawing unsolved problems at random (the first round drawn this way) · The ledger of claims · The Lean verification bundle · The Lean guide