Proved
Formal deduction from Bombieri–Vinogradov ↗
The implication to the 246 bound, not a Lean proof of its analytic premise.
PrimeGapsLib: a formal deduction of the 246 bound · README main results; PrimeGaps/Bounded246.lean →
Observed Oct 13, 2026
Theorem · version 1
Bombieri–Vinogradov implies recurring gaps at most 246
Statement
Assuming the precise BombieriVinogradov statement in PrimeGapsLib, infinitely many consecutive-prime gaps are at most 246.
Assumptions
- The source’s formal BombieriVinogradov premise.
Scope
The certificate and downstream sieve deduction are formalized; the analytic distribution theorem is a premise in this endpoint.
Evidence
Source reports
Formal proofs
Lean: 246 from Bombieri–Vinogradov ↗
Complete formal proof reported externally
Complete as an implication with the stated premise. This is the public 246 artifact, not the later reported 212 certificate.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Declaration & revision
bombieriVinogradov_implies_frequently_prime_gap_le_246Commit 1faa7b14e82ddebc2772dfb9153922f01b106477
Connections
In this problem · publication v4 · Selected context
How small can prime gaps be? →
Conditional result · Proved
Scope: The public Lean endpoint formalizes the deduction to 246 from Bombieri–Vinogradov.
Limit: The cited mathematical 246 result is unconditional, but this formal endpoint does not prove its analytic premise.
Nested results concern the same prime-gap limit; they are not separate portions of a solved problem.
Related results · 1
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v7
How small can prime gaps be? →
Conditional result · Proved
Scope: The public Lean theorem formalizes the deduction to 246 from Bombieri–Vinogradov.
Limit: The cited mathematical 246 result is unconditional, but this formal theorem does not prove its analytic premise.
Nested results concern the same prime-gap limit; they are not separate portions of a solved problem.
Related results · 1
Relationship not independently reviewed. This concerns its use in this problem.
Sources
PrimeGapsLib: a formal deduction of the 246 bound →
- README main results; PrimeGaps/Bounded246.lean → · Original passage ↗
Recorded wording
The public revision proves prime-gap bounds of 246 assuming Bombieri–Vinogradov and includes numerical certificates. It does not contain the 212 formalization reported in the later paper.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
Axiom Math · PrimeGapsLib contributors · Project documentation · Publication date Aug 18, 2026
Public formal source; build and independent mathematical review are separate checks.
PrimeGapsLib: a formal deduction of the 246 bound — pinned source ↗No OpenMath execution recorded
Public source inspected for statement and assumptions; this proof project has not been executed by OpenMath.
Revision & attribution
Source revision: 1faa7b14e82ddebc2772dfb9153922f01b106477. Observed Oct 13, 2026.
Axiom Math’s formalization work concerns proof translation and certificates; no independent discovery credit is assigned from the repository alone.
Source updated Aug 18, 2026.
PrimeGapsLib: a formal deduction of the 246 bound — pinned source: 1faa7b14e82ddebc2772dfb9153922f01b106477.
Variants of the Selberg sieve, and bounded intervals containing many primes →
- Main bounded-gap results and introduction → · Original passage ↗
Recorded wording
The published Polymath8b argument establishes an unconditional recurring prime gap at most 246; the twin-prime target remains out of reach.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
D. H. J. Polymath · Published · Publication date 2014
Peer-reviewed historical result.
Revision & attribution
Source revision: 2014. Observed Oct 13, 2026.
No AI contribution is asserted by this source record.
History
Statement versions
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessment history · 1
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Formal deduction from Bombieri–Vinogradov ↗
The implication to the 246 bound, not a Lean proof of its analytic premise.
Observed Oct 13, 2026 · Source passage →
Record details
- Claim ID
- claim-prime-gaps-bv-implies-246
- Statement version
- 1
- SHA-256
- 3ee9cfe45206a3759bd9c4cd0aee5414e216ee6bd63226c3845af54aff0c98f3