OP-00020 Open

The Gaussian moat problem

Is there an infinite sequence of distinct Gaussian primes $x_1, x_2, \ldots$ such that $\lvert x_{n+1} - x_n \rvert$ is bounded? Equivalently, can one walk to infinity through the Gaussian primes taking steps of bounded length?

Source: Basil Gordon (ICM Stockholm, 1962); often misattributed to Erdős. See Gethner, Wagon and Wick, A stroll through the Gaussian primes, Amer. Math. Monthly 105 (1998); erdosproblems.com/952.

Classification

Primary: NT — Number Theory
Keywords: Erdős problems, Gaussian primes

References

@article{gww1998,
  author = {Gethner, Ellen and Wagon, Stan and Wick, Brian},
  title = {A stroll through the {G}aussian primes},
  journal = {American Mathematical Monthly},
  volume = {105},
  pages = {327--337},
  year = {1998}
}

@article{jordanrabung1970,
  author = {Jordan, J. H. and Rabung, J. R.},
  title = {A conjecture of {P}aul {E}rd{\H{o}}s concerning {G}aussian primes},
  journal = {Mathematics of Computation},
  volume = {24},
  pages = {221--223},
  year = {1970}
}

@misc{erdosproblems952,
  title = {Erdős Problem \#952},
  howpublished = {erdosproblems.com},
  url = {https://www.erdosproblems.com/952}
}

@misc{wikipedia,
  title = {Gaussian moat},
  howpublished = {Wikipedia},
  url = {https://en.wikipedia.org/wiki/Gaussian_moat}
}

@misc{formalconjectures,
  author = {{The Formal Conjectures Authors}},
  title = {Formal Conjectures},
  url = {https://github.com/google-deepmind/formal-conjectures/blob/0771383387505c96d1b2f6a3d35088ad00892c5c/FormalConjectures/ErdosProblems/952.lean#L33},
  note = {Lean statement under Apache-2.0; problem text under CC BY 4.0, or CC BY-SA 4.0 where it is based on Wikipedia}
}

Canonical Lean statement

A submission resolves this problem by proving the constant Problem_OP_00020.

/-- OP-00020: The Gaussian moat problem -/
def Problem_OP_00020 : Prop :=
  ∃ (x : ℕ → GaussianInt) (C : ℤ),
      Function.Injective x ∧ ∀ (n : ℕ), Prime (x n) ∧ Zsqrtd.norm (x (n + (1 : ℕ)) - x n) < C

Formalised by The Formal Conjectures Authors (Apache-2.0); reviewed by clemens-admin.

Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.

Resolving this problem in Lean

Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.

In lakefile.toml:

[[require]]
name = "RegistryProblems"
git = "https://github.com/cthalhammer/registry-problems"
rev = "<published revision>"

In your proof:

import RegistryProblems.OP_00020

theorem resolution : RegistryProblems.Problem_OP_00020 := by
  sorry

In preprint.toml, mapping the claim to the declaration that establishes it:

[[statements]]
label = "Theorem 1"
lean = "resolution"
latex = "..."
problem = "OP-00020"
claim = "full"

To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:

theorem disproof : ¬ RegistryProblems.Problem_OP_00020 := by
  sorry

You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.

Citing this problem

This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.

OP-00020, "The Gaussian moat problem", clopen.solutions.