SIGNIFICANCE

Checked 2026-08-31 · source current · v1

Claim recorded by DottedCalculator

What is claimed?

A Tilted Residue-Class Construction for Long Prime-Free Intervals claims Y(X) ≫ X log X / log₃ X and G(T) ≫ log T log₂ T / log₄ T.

Quoted from the source · dottedcalculator · 2026-08-26 · View source

Component dates
Preprint
2026-08-25
Exposition
Not recorded
Formalization
2026-08-27

Component dates (preprint / exposition / formalization). Formalization date from the artifact reported by the source. “Not recorded” means no dated source is recorded for that component. Preprint dates refer to the pinned manuscript version.

Reader summary

Claimed
The 48-page manuscript reports a new tilted preliminary sieve and claims lower bounds Y(X) ≫ X log X / log₃ X and G(T) ≫ log T log₂ T / log₄ T.

Reader summary · Significance · 2026-08-31

What has been checked?

Significance pinned and hashed the submitted PDF, inspected the public discussion, and located a commit-pinned external Lean proof and kernel-axiom audit. Ben Green's public comments are recorded as an attributed informal review, not as a Significance conclusion.

Reader summary · Significance · 2026-08-31

Independent reruns
0
Math assessments
0
Written reviews
1

Where is help needed?

Significance has not independently rebuilt the Lean project, audited paper-to-Lean correspondence, or checked the manuscript's sieve argument. The forum's formalization link and the repository's completed proof also point to different files, as recorded below.

Reader summary · Significance · 2026-08-31

See 2 open checks →

Problem link

ErdősProblems.com #4 · open the original problem page

Quoted from the source · Significance editor · 2026-08-31 · View source

Author involvement

Compiled from the public proof claim, pinned manuscript, public discussion, and public Lean repository. DottedCalculator and the named commenters have not reviewed or confirmed this Significance record.

Record note · Significance · 2026-08-31

Start here · for reviewers

Main deduction

Begin with Section 3 and then the correlation work in Sections 4–5. The proposed new mechanism replaces the hard cutoff in the second sieve with a tilted probability law; later FGKMT gains are intended to remain independent and therefore multiply with it.

Sections 3–5 · Xiao Hu's description of the modified second sieve; Ben Green's reply on where the new work sits. · Quoted from the source · xiao hu · 2026-08-28 · View source

Risk points

  • The manuscript itself says its conclusion depends on the cited deep inputs being available with exactly the uniformity stated; the assembly and transfer steps cannot repair a missing input.

    Introduction, page 3; Section 6.2 · Quoted from the source · dottedcalculator · 2026-08-25 · View source

  • Sections 6.6–6.8 track FGKMT Sections 6 and 8, Section 7 expands a short FGKMT assembly argument, and Section 8 is the elementary CRT transfer. Readers already fluent in FGKMT can separate these passages from the claimed new sieve.

    Sections 6.6–8 · Quoted from the source · xiao hu · 2026-08-28 · View source

Useful background

  • The Ford–Green–Konyagin–Maynard–Tao 2018 construction, especially the multidimensional sieve estimate and quantitative hypergraph covering theorem used in Section 6.

    FGKMT 2018; manuscript Section 6.2 · Significance’s interpretation · Significance editor · 2026-08-31

Needs checking

  • Compare the two manuscript inequalities with Erdos4.Tilted.covering_theorem and Erdos4.Tilted.prime_gap_corollary at commit 554ac598, including all definitions of Y, G, and endpoint conventions. — A successful Lean build and exact statement correspondence are separate questions, and neither has been independently recorded here.

    PDF equations (1.2)–(1.3); Erdos4Tilted.lean · Significance’s interpretation · Significance editor · 2026-08-31

  • Resolve the public link mismatch: Boris Alexeev's forum hyperlink lands on ComparatorChallenges/ErdosProblems/Erdos4.lean, whose declarations use sorry at the pinned commit, while the completed proof and guarded axiom audit live under src/latest/ErdosProblems. — The artifact is present, but a reader following only the posted link is taken to the wrong file.

    Forum post 8611; comparator file; Erdos4Tilted.lean; TiltedVerification.lean · Automated result · Significance editor · 2026-08-31

  • Suggest another focused check

Formalization handoff

A compact map for someone who wants to formalize this claim. It records preparation and open work, not a mathematical verdict.

Target
The covering theorem Y(X) ≫ X log X / log₃ X and the endpoint prime-gap corollary G(T) ≫ log T log₂ T / log₄ T. Quoted from the source · boris alexeev · 2026-08-27 · View source
System
Lean 4.33.0 with Mathlib 4.33.0, as recorded by the pinned repository. Quoted from the source · boris alexeev · 2026-08-27 · View source
Work state
Artifact reported
Code
formalization repository · commit 554ac598b287… · Lean 4.33.0; Mathlib 4.33.0

Definitions

  • Compare maximumCoverLength and maximumPrimeGap with the manuscript's Y and G, including the use of real frontiers and right-endpoint bounds.

    Significance’s interpretation · Significance editor · 2026-08-31

Prerequisites

  • The pinned src/latest project, the Erdos4Tilted import tree, and the repository's TiltedVerification.lean axiom audit.

    Significance’s interpretation · Significance editor · 2026-08-31

Open questions

  • Can an independent build reproduce the reported final theorems and guarded axiom output at commit 554ac598?

    Significance’s interpretation · Significance editor · 2026-08-31

  • Does the full import closure correspond to every non-classical input and uniformity condition used by the pinned manuscript?

    Significance’s interpretation · Significance editor · 2026-08-31

Paper/code correspondence: The pinned Lean source names the manuscript and states matching displayed asymptotic bounds, but Significance has not independently audited every definition or dependency across the paper and code. Significance’s interpretation · Significance editor · 2026-08-31

Significance’s interpretation · Significance editor · 2026-08-31

Careful wording

A public manuscript claims a stronger lower bound for long prime gaps; a separate Lean repository reports a completed formalization, and Ben Green has published a favorable but informal assessment after discussions with Terry Tao and James Maynard.

Wording · Significance · 2026-08-31

Copy for sharing

Copy and paste this summary.

A public manuscript claims a stronger lower bound for long prime gaps; a
separate Lean repository reports a completed formalization, and Ben Green
has published a favorable but informal assessment after discussions with
Terry Tao and James Maynard.

Checked: Significance pinned and hashed the submitted PDF, inspected the
public discussion, and located a commit-pinned external Lean proof and
kernel-axiom audit. Ben Green's public comments are recorded as an
attributed informal review, not as a Significance conclusion.

Not checked: Significance has not independently rebuilt the Lean project,
audited paper-to-Lean correspondence, or checked the manuscript's sieve
argument. The forum's formalization link and the repository's completed
proof also point to different files, as recorded below.

As of 2026-08-31T01:02:46Z (freshness: current)
Full record: https://hjyuh.github.io/significance/2026-dottedcalculator-erdos-4/
Significance records evidence. It does not judge the mathematics.
Scope
ErdősProblems.com classifies this as a partial proof claim: it proposes a stronger lower bound beyond the established solution of the original problem, not a new resolution of the page's already-proved statement. Quoted from the source · dottedcalculator · 2026-08-26 · View source
Source
A Tilted Residue-Class Construction for Long Prime-Free Intervals · github-dottedcalculator-ai-math-9ed1cea5 · retrieved 2026-08-31T01:02:46Z
sha256 c124e109dba9…

Evidence: 3 entries

  1. Source inspection

    ev-source-inspection

    Public-source and version check only. This is not a mathematical review.

    Significance fetched the proof-claim page, its 48-page PDF, the sixteen public discussion comments, and the referenced Lean repository. The PDF was pinned to commit 9ed1cea5 and hashed. This records sources and versions, not a mathematical review.

    Automated result · Significance editor · 2026-08-31 · View source

  2. Formal code published by the source

    ev-lean-artifact-reported

    Published by the source. Any independent rerun appears as a separate entry.

    Boris Alexeev publicly reported an unconditional Lean formalization. At the pinned commit, the completed covering and prime-gap theorems are in src/latest/ErdosProblems/Erdos4Tilted.lean, with guarded axiom output in src/latest/ErdosProblems/Erdos4/TiltedVerification.lean. Significance has inspected those files but has not independently built the project.

    Open link @ 554ac598b287… · Quoted from the source · boris alexeev · 2026-08-27 · View source

  3. Written review

    ev-ben-green-informal-review

    After several hours of thought and conversations with Terry Tao and James Maynard, Ben Green wrote that he was more or less convinced by the claim; he also distinguished the existence of the Lean formalization from the remaining work of producing a readable human exposition.

    Quoted from the source · ben green · 2026-08-27 · View source

Plain-language explanation

The original Erdős question on this page was already solved. This record concerns a stronger claimed lower bound: a different preliminary sieve is proposed before the established FGKMT machinery is applied. The most useful first reading is therefore Sections 3–5, not the full 48 pages in order.

Explanation · Significance

Importance

Before this submission, ErdősProblems.com listed the FGKMT 2018 bound as the best available lower bound for the problem. Quoted from the source · Significance editor

Ben Green described the tilted sieve and the FGKMT gain as essentially independent improvements over the older Erdős–Rankin procedure. Quoted from the source · ben green

The ErdősProblems.com page says the likely scale is comparable to (log n)^2 and that the later $10,000 target asks for a lower bound above (log n)^(1+c); the submitted claim does not reach that target. Quoted from the source · Significance editor

The same page records the best known upper bound for consecutive prime gaps as p_(n+1) − p_n ≪ n^(0.525+o(1)), due to Baker, Harman, and Pintz. Quoted from the source · Significance editor

Limits of this record
  • This record does not issue a whole-paper correctness judgement.
  • Reviews and assessments are attributed conclusions by their writers, not conclusions issued by Significance.
  • Open invitations identify work not yet represented by a completed evidence entry.