erdos_470.variants.prime_gap_imp_inf_prim_weird

Specification

Melfi [Me15](https://mathscinet.ams.org/mathscinet/relay-station?mr=3276337) has proved that there are infinitely many primitive weird numbers, conditional on the fact that $p_{n+1} - p_n < \frac{1}{10} \sqrt{p_n}$ for all large $n$, which in turn would follow from well-known conjectures concerning prime gaps.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof

Lean 4 Statement

theorem erdos_470.variants.prime_gap_imp_inf_prim_weird :
    ∀ᶠ n in Filter.atTop, primeGap n < √ (n.nth Nat.Prime) / 10 →
      Set.Infinite PrimitiveWeird

ID: ErdosProblems__470__erdos_470.variants.prime_gap_imp_inf_prim_weird

Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →

Docs

Verification Pipeline

How zero-trust verification works.

Read docs →

Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.