A Reduction of Guy's Problem D18 to a Genus 5 Fibration over a K3 Surface

Abstract

Guy's Problem D18 asks whether there exist four distinct positive integers whose squares have all pairwise differences equal to perfect squares. We prove that this problem is equivalent to the existence of a non‑trivial rational point on a family of genus 5 curves fibered over a K3 surface. The reduction is algebraic and explicit: the six square conditions are decoupled into a semi‑perfect cuboid (parameterized by the K3 surface) and a simultaneous pair of quartic equations. Their quotient by the involution X ↦ -X yields a genus‑1 base, and the original double cover has genus 5 by Riemann–Hurwitz. Faltings’s theorem then guarantees finitely many rational points on each fiber, turning the original infinite search into a finite computation. All core algebraic identities have been formally verified in Lean 4, and we find no local obstruction for small primes, so the difficulty is entirely global. This reformulation embeds a classical recreational problem into the rigorous framework of modern arithmetic geometry.