VibeMathed reports this item as partial. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
For the sequence of primes $p_n$, the project derives
$$\liminf_{n\to\infty}(p_{n+1}-p_n)\le186.$$
More precisely, assuming three explicit analytic/numerical inputs, it proves $\mathrm{DHL}[40,2]$: every admissible set of forty integer shifts has infinitely many translates containing at least two primes. Applying this to an explicit admissible $40$-tuple of diameter $186$ yields infinitely many consecutive prime gaps of size at most $186$. The Lean development verifies the deduction from the stated inputs; the two Kloosterman-type estimates and the finite physical-integral/cap bounds remain external assumptions.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
GPT 6 Astra
The project metadata identifies GPT 6 Astra, operating through Codex, as the agent used for the formalization workflow. Its stated task was to formalize the source statements faithfully, simplify the proofs, and retain unresolved finite-field and numerical inputs as explicit axioms. The resulting development was refined through human-guided edits and automated proof checks. The repository metadata attributes both the project and its source article “Improved Gaps Between Primes” to OpenAI.
Lean-checked, not Lean-verified, and the distinction is the whole of it. The Lean development in openai/PrimeGaps186 reports zero sorry in its three main declarations, and Comparator and Lean's kernel accept them - but all three depend on three project-specific axioms: a rank-three hyper-Kloosterman bound, a rank-two Kloosterman correlation bound, and a package of 104 outer, 45 inner and 3 cap numerical inequalities. So the kernel has checked that those three statements imply DHL[40,2] and the bound; it has not checked them. The first two are tied to established literature and the third is recomputed by a Python and FLINT certificate that does not discharge its Lean axiom. No independent expert has read the paper on the record.
Assuming three explicit input statements, the project proves $\mathrm{DHL}[40,2]$: every admissible $40$-tuple contains at least two primes infinitely often after translation. An explicit admissible $40$-tuple of diameter $186$ then gives
$$\liminf_{n\to\infty}(p_{n+1}-p_n)\le186.$$
The Lean proof of the implication from the three inputs to the final theorem is kernel-checked. Two inputs are Kloosterman-type estimates cited to Katz/Deligne and Fouvry--Kowalski--Michel; the third consists of finitely many numerical integral and cap inequalities backed by a Python/FLINT certificate.
Known method families
construction (source-reported)
Source-reported tools: construction.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.