How to Formally Verify a New Prime-Gap Record

Distinguishing a Record from a Proof

Research on prime gaps often aims to prove that, beyond a sufficiently large range, there are consecutive primes whose gap is no greater than a certain upper bound. A smaller bound generally represents a stronger result. However, seeing a smaller number does not immediately mean that a related conjecture has been solved or that an unconditional proof has been completed.

When evaluating such claims, at least three questions must be separated:

1. What exactly has been proved? Is the result an upper bound for some prime gap, or does it resolve the twin prime conjecture? Even a significant improvement to an upper bound does not prove that infinitely many pairs of primes differ by a fixed value.
2. Does the conclusion depend on assumptions? If the derivation uses estimates that have not been established within the current proof, the result is conditional rather than an unconditional theorem.
3. What does the verification cover? A machine checker may verify the logical steps of a derivation without validating every input assumption. It also cannot automatically replace the mathematical community’s review of external lemmas.

Therefore, when encountering a claim about a “new record,” the first priority should be the formal statement and its dependencies—not just the number highlighted in the headline.

What Formal Proof Can Verify

A formal proof encodes mathematical definitions, propositions, and inferences in a rigorous logical system. A trusted kernel then checks whether every step follows according to the system’s rules. This can reduce gaps in a reasoning chain and make the proof structure easier to review and reuse.

Formalization does not, however, automatically prove every mathematical fact from first principles. A large formal proof typically invokes existing theorems, definitions, or explicitly listed axioms. If the system accepts a proposition as a premise, it can rigorously check whether the target follows from that premise, but it does not thereby prove that the premise itself is true.

The structure can be abstracted as follows:

Premises A, B, and C hold
The derivation follows the rules of logic
Therefore, conclusion T follows

If a verifier checks the derivation successfully, the supported claim is that T follows from A, B, and C. To upgrade this to an unconditional conclusion, it is also necessary to establish that A, B, and C have been proved, or to state clearly that they are accepted foundational assumptions.

This distinction is not a weakness of formalization. It is how a logical system is supposed to work. Formal tools are well suited to checking whether an inference is valid. The applicability of the premises, the accuracy of citations, and the correctness of the mathematical model still require separate review.

Why External Lemmas Matter

Results in analytic number theory often depend on complicated estimates, such as bounds for exponential sums, character sums, or multiple integrals. A complete proof may be divided into several layers: first establishing analytic estimates, then using a sieve or another method to derive a conclusion about prime gaps.

A formalization project may encode the latter part of the derivation in considerable detail. But if the earlier estimates are supplied as external propositions, the reliability of the final conclusion depends on the origin and accuracy of those propositions.

At a minimum, an external lemma should be checked for the following:

• Consistency of the statement: Do the variable ranges, parameter conditions, error terms, and limiting processes in the cited result exactly match the formalized version?
• Satisfaction of applicability conditions: A theorem may require smoothness, coprimality, range restrictions, or other properties. Each condition must be verified when the theorem is applied.
• Matching constants and normalization: Different sources may use different notation, measures, integration domains, or conventions for constants. These conversions cannot be silently omitted.
• Completeness of the citation chain: If a lemma depends on earlier results, those dependencies should be traceable to proofs that can be checked, rather than relying only on a secondary summary.
• Faithfulness of the formal statement: The definitions used in the code must correspond to the mathematical objects in the paper, especially in boundary cases and under implicit conventions.

Listing a bibliographic source is not the same as completing this verification. Likewise, the fact that an external lemma has not been reproved in the same formal system does not automatically invalidate the overall work. The essential requirements are to disclose the dependencies and describe the conditional status of the result accurately.

The Limits of Numerical Certificates and Derivation Checks

Some proofs convert a continuous problem into computable integrals or inequalities and then use scripts to generate and verify a finite set of numerical certificates. This can improve reproducibility and reduce the risk of manual calculation errors. However, a script completing successfully only shows that it processed its inputs according to the specified rules. It does not, by itself, prove that the model is correct or that all mathematical assumptions hold.

For example, if a proof uses a function (F) to construct a square integral and marginal integrals, the relevant quantities might take forms such as

[
Ik(F)=\int{[0,1]^k} F^2(t_1,\ldots,t_k)\,dt_1\cdots dt_k,
]

[
Jk^{(m)}(F)=
\int{[0,1]^{k-1}}
\left(\int0^1 F(t_1,\ldots,t_k)\,dt_m\right)^2
\prod{i\ne m}dt_i.
]

Even if a program computes valid bounds for these quantities, reviewers must still confirm that the function belongs to the required class, that the integration variables are defined correctly, that numerical errors are controlled, and that the final conclusion genuinely follows from the integral estimates.

A numerical certificate is one component of the proof chain—not a substitute for the entire proof.

How to Evaluate a Claim of a New Record

A careful review can be organized into four steps.

Step 1: Locate the precise proposition. Record the claimed upper bound, its range of applicability, and any additional conditions. Determine whether the statement concerns infinitely many cases or only a finite computational range. Do not confuse an improvement to a known bound with the resolution of a conjecture.

Step 2: Map the dependency graph. Break the target into the main theorem, auxiliary lemmas, external estimates, and computational certificates. Mark which parts are proved in the current system, which are imported from the literature, and which remain explicit assumptions. This reveals exactly which section of the proof chain has been machine-checked.

Step 3: Review the reproducibility materials. Independently examine the formal files, scripts, input data, and build instructions. Confirm that the result does not depend solely on an undisclosed environment or undocumented manual steps. Successful reproduction increases confidence in the implementation, but it does not replace the review of the mathematical premises.

Step 4: Check accountability and wording. Named authors, review records, and a clear process for reporting errors make it easier for the community to identify problems. Publishers should distinguish among a derivation that has been formally verified, a result that depends on established theorems, and an assumption that remains to be checked. A vague claim that the “proof is complete” can conceal important differences between these states.

How to State the Conclusion More Precisely

If a key input is still provided as an assumption, the rigorous formulation should say that, under the listed premises, the formalized derivation establishes a particular upper bound. It should also state that the correctness and applicability of those premises still need to be checked against the original proofs.

If an external estimate has already been established by independent research, the result should identify the supporting reference and its applicability conditions. Readers should not be left with the impression that every part was proved from first principles within the same formal system.

This does not diminish the value of formalization. Breaking down a complex derivation, documenting its dependencies precisely, and subjecting the logical steps to machine checking are all important achievements in mathematical engineering. Formalization can also expose hidden assumptions and help researchers identify the parts of a proof that deserve the closest review.

Still, “the reasoning chain has been checked” and “the entire mathematical argument is unconditionally valid” describe two different levels of certainty. Public communication must keep them separate.

The evaluation of a new prime-gap result should ultimately return to the precise proposition, the complete dependency chain, and clearly assigned proof responsibilities. Whether a number sets a new record is only the starting point. The strength of the conclusion depends on whether every premise holds, whether every step is applicable, and whether the published materials allow others to perform an independent review.