Number theory · Last catalog review 26 Jul 2026

Erdős Problem 952

Is there an infinite sequence of distinct Gaussian primes

x_1,x_2,\ldots

such that

\lvert x_{n+1}-x_n\rvert \ll 1

References

Published 10 Jun 2026Never attempted

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-e923379e-erdos952-erdos-952-700fa83d72-formalized-v1
Task commitment: sha256:4bd1813dd86f0b43c7c7247ab9c36420787fa5cb126a638bcac11038bb2a9fd3

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.