Conjectures.io

Number theory

Erdős 853 - part i

Let dn=pn+1−pnd_n = p_{n+1} - p_n, where pnp_n is the nnth prime. Let r(x)r(x) be the smallest even integer tt such that dn=td_n = t has no solutions for n≤xn \le x. Is it true that r(x)→∞r(x) \to \infty?

References

No one has attempted this yet.

Formal statement

Lean type

Filter.Tendsto Erdos853.r Filter.atTop Filter.atTop

What you must prove

import FormalConjectures.ErdosProblems.«853»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos853.erdos_853.parts.i" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/853.lean

Source type SHA-256
sha256:c72053a2605d719f8d714ce5f6eb15c7295915419038572a2c4be0a80e3a0dad
Task id
fc-379fc029-parts-i-9cb1cc3ec6-formalized-v1
Task commitment
sha256:f11caec9ab40a1b44120c6aa5229a0d2bc7b5fd574ea60e07fc3df40568dc9ba

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.