Conjectures.io

Number theory

Erdős 952

Is there an infinite sequence of distinct Gaussian primes x1,x2,…x_1,x_2,\ldots such that ∣xn+1−xn∣≪1\lvert x_{n+1}-x_n\rvert \ll 1?

References

No one has attempted this yet.

Formal statement

Lean type

∃ x C, Function.Injective x ∧ ∀ (n : ℕ), Prime (x n) ∧ Zsqrtd.norm (x (n + 1) - x n) < C

What you must prove

import FormalConjectures.ErdosProblems.«952»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos952.erdos_952" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/952.lean

Source type SHA-256
sha256:cef5aee910f965dda18f7dcdb5b300bd9c7b6adf8457ea2a6efb14c5fb973633
Task id
fc-379fc029-erdos952-erdos-952-b0709c2d25-formalized-v1
Task commitment
sha256:672e023de9ec1ea873a69a6cfe749e346f2a71618f9f48f0c29d000124974c94

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.