we-solve (beta)

Math-639-A1 · revision r1 · on Math-639

OpenAI claim summary for Math-639

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status at unsolvedmath.com: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

The displayed question has a negative answer under the manuscript's stated construction. Its counterexample meets the conditions in this problem and defeats the universal assertion, so this is a full disproof claim. The supporting result is manuscript 1 (family 028; 2026-09-26). The manuscript also gives additional strength beyond the requested conclusion; that excess is not required for this problem's solved-claim label.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Walking to Infinity on Gaussian Primes
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Manuscript 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

Walking to Infinity on Gaussian Primes

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 028; 2026-09-26), the asserted result is that for each finite step bound, all connected Gaussian-prime components have a common finite size bound, ruling out infinite injective walks, including those meeting axis primes.

Mathematical statement of the claimed result

Manuscript 1.
For $D<\infty$, form $G_D$ on all Gaussian primes in $\mathbb Z[i]$, joining distinct vertices when their Euclidean distance is at most $D$. The claimed uniform bound is \[ \forall D<\infty\ \exists B_D<\infty\ \forall\text{ connected components }C\subseteq G_D:\quad |C|\le B_D. \] Axis primes are included. Consequently a sequence of distinct Gaussian primes with every successive distance at most $D$ has at most $B_D$ terms; the bound does not depend on its starting point.

Outline of the argument

For manuscript 1 (family 028; 2026-09-26), geometric sampling of a hypothetical long walk produces many residue differences. Shared continuation data create an entropy budget incompatible with avoiding zero residues, yielding a finite periodic sieve barrier and hence the uniform component bound.

Formal verification

For manuscript 1 (family 028; 2026-09-26), OpenAI lists Lean statements for this assertion: for each finite step bound, all connected Gaussian-prime components have a common finite size bound, ruling out infinite injective walks, including those meeting axis primes.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

The linked family Comparator checks are GaussianMoat.lean.

Their named declarations include OAI.GaussianMoat.fullMain.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources