Oct 6, 2026
Lean formalization in OpenAI math repository (Result 028)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Bounded-Step Walks on Gaussian Primes'. We prove the Gaussian moat conjecture: no infinite walk through distinct Gaussian primes can have bounded steps. More strongly, for each fixed finite step bound, the connected components of the Gaussian-prime graph have uniformly bounded size. This bound applies to every starting prime, including primes on the coordinate axes, and is nonexplicit. The proof constructs a finite periodic sieve obstruction using geometric sampling and information-theoretic estimates.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 028). The Lean development was not rebuilt locally.