Reading source record 1faa7b14e82ddebc2772dfb9153922f01b106477. View default cited record →
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.
Public formal source; build and independent mathematical review are separate checks.
1 cited passage ↓1 problem ↓Record 1faa7b14e82ddebc2772dfb9153922f01b106477 ↓
The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.
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.
Passage ID: prime-gaps:entry:246-lean:v1
Source item: 246-lean
Source record: prime-gaps:source:246-lean:v1
Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.
Problem publication v7
Source assessment
Proved
Formal deduction from Bombieri–Vinogradov
The implication to the 246 bound, not a Lean proof of its analytic premise.
Observed Oct 13, 2026
Formal declaration
Lean: 246 from Bombieri–Vinogradov
History
A public formal deduction for 246
Question
How small can prime gaps be?
Further reading
Inspect the formal statement, assumptions and reported checks.
Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.
Formal code
No OpenMath execution recorded
Public source inspected for statement and assumptions; this proof project has not been executed by OpenMath.
Resource revision: 1faa7b14e82ddebc2772dfb9153922f01b106477
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
bombieriVinogradov_implies_frequently_prime_gap_le_246Commit 1faa7b14e82ddebc2772dfb9153922f01b106477
Recorded authorship
Axiom Math · PrimeGapsLib contributors
Axiom Math, PrimeGapsLib contributors
Axiom Math’s formalization work concerns proof translation and certificates; no independent discovery credit is assigned from the repository alone.
OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.
PrimeGapsLib: a formal deduction of the 246 bound
OpenMath supplies original paraphrases and links; no proof text is republished.
Source terms ↗