The key number-theoretic reduction lemma (Lemma 3.1) is formalized in Lean 4 using Aristotle, building on an existing Lean formalization of the unit-distance disproof.
Abstract
Several fundamental problems in computational geometry admit algorithms with running time $f(d) \cdot n^{2-Θ(1/d)}$ for $n$ points in $d$ dimensions, making them among the most prominent examples of barely subquadratic computation. Notable members of this class include Furthest Pair, Bichromatic Closest Pair, (Bichromatic) Maximum Innter Product, and Hopcroft's Problem. Chen [Theory Comput. 2020] proved that, assuming the Strong Exponential Time Hypothesis (SETH), these problems require $n^{2-o(1)}$ time when the dimension satisfies $d=2^{Θ(\log^* n)}$. We extend this lower bound to all efficiently constructible dimensions $d=ω(1)$. Thus, assuming SETH, the dependence of the best known algorithms on the dimension is essentially unavoidable. The proof utilizes techniques in OpenAI's recent disproof of the Erdos unit distance conjecture. The proof was initially discovered by ChatGPT 5.5 Pro. The authors have validated and substantially edited the proof to improve the presentation.
Problem
Furthest Pair, Bichromatic Closest Pair, Max Inner Product and Hopcroft's problem have f(d)·n^{2-Θ(1/d)} algorithms. Earlier SETH lower bounds only covered dimension d=2^{Θ(log* n)}. The open question was whether quadratic hardness holds for every superconstant dimension.
Approach
An improved local reduction from Boolean OV to Z-OV is built with algebraic number theory: number fields, prime ideal valuations, and class field towers, following techniques from OpenAI's disproof of the Erdős unit distance conjecture. A CRT composition step then makes the reduction uniform. The proof was first found by ChatGPT 5.5 Pro and then edited by the authors. Lemma 3.1 was formalized in Lean 4 with Aristotle, assuming Golod–Shafarevich, Shafarevich relation-rank and Chebotarev density hypotheses.
(a)
Results
Under SETH, these problems require n^{2-o(1)} time for every efficiently constructible dimension d=ω(1). The Lean 4 formalization of Lemma 3.1 is released at github.com/xuyinzhan/max-ip-lean.
