Number theory

Erdős 218 - le

The set of indices

n

for which a prime gap is followed 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 ≤ primeGap (n + 1)}.HasDensity (1 / 2)

What you must prove

import FormalConjectures.ErdosProblems.«218»
import TaskSupport

namespace Bounty

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

end Bounty

Pinned source: FormalConjectures/ErdosProblems/218.lean

Source type SHA-256: sha256:500fe5b6e6370b9dac095765a9e6da3ac8955c9c279ab3151b35de4884cebead
Task id: fc-379fc029-variants-le-c9fd7391ce-formalized-v1
Task commitment: sha256:9b4f2d1d66a780443aba226926f9d22763dcc7ef17866ac1ef7bc985b1dc382f

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.