Number theory

Erdős 218 - ge

The set of indices

n

for which a prime gap is preceeded by a larger or equal prime gap has a natural density of

\frac 1 2

References

erdosproblems.com/218

No one has attempted this yet.

Formal statement

Lean type

{n | primeGap (n + 1) ≤ primeGap n}.HasDensity (1 / 2)

What you must prove

import FormalConjectures.ErdosProblems.«218»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos218.erdos_218.variants.ge" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/218.lean

Source type SHA-256: sha256:e18230aa1dec34ab29027eee7e5a34159aa4a7b0d8e46c2488bae34af3ad0cd8
Task id: fc-379fc029-variants-ge-5c86387d13-formalized-v1
Task commitment: sha256:7847ae51b0926f7d0819018988390f2e39a4b475234897a43a3b1aba3f1e424a

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.