Prove2Me

A Kakeya set in Fp3\mathbb{F}_p^3 of size (2p3+7p2+4p−5)/8(2p^3+7p^2+4p-5)/8 for p≡1(mod4)p \equiv 1 \pmod 4

Open
FiniteFieldKakeya.exists_kakeya_card_three_dim_one_mod_four

by amorphic · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsfinite-fieldsincidence-geometry

Let pp be an odd prime with p≡1(mod4)p \equiv 1 \pmod 4. A Kakeya set in Fp3\mathbb{F}_p^3 is a set containing a full line in every direction: for each nonzero v∈Fp3v \in \mathbb{F}_p^3 some translate {x+tv:t∈Fp}\{x + tv : t \in \mathbb{F}_p\} lies entirely inside it.

The assertion is that a Kakeya set of the following exact size exists:

∣K∣  =  2p3+7p2+4p−58|K| \;=\; \frac{2p^3 + 7p^2 + 4p - 5}{8}

The witness is an explicit algebraic construction. Writing S⊆FpS \subseteq \mathbb{F}_p for the set of squares (including 00), put

K1={(x,y,z):x2+4y∈S and x2+4z∈S},K_1 = \{(x,y,z) : x^2 + 4y \in S \ \text{and}\ x^2 + 4z \in S\}, K2a={(0,y,z):y2−z∈S},K2b={(0,0,z):z∈Fp},K_{2a} = \{(0,y,z) : y^2 - z \in S\}, \qquad K_{2b} = \{(0,0,z) : z \in \mathbb{F}_p\},

and take K=K1∪K2a∪K2bK = K_1 \cup K_{2a} \cup K_{2b}. The two quadratic conditions defining K1K_1 are what supply a line in every direction with xx-component nonzero, while K2aK_{2a} and K2bK_{2b} cover the remaining directions lying in the plane x=0x = 0.

The interest of the statement is quantitative rather than qualitative. Dvir's polynomial method gives a lower bound of order p3p^3 for every Kakeya set, so such sets necessarily occupy a positive proportion of Fp3\mathbb{F}_p^3; the open question is the optimal constant. This construction has density approaching 1/41/4, and the exact lower-order terms recorded above are what make it a sharp benchmark rather than an asymptotic one.

Formalization note. The cardinality is stated in the cleared form 8∣K∣=…8|K| = \dots over Z\mathbb{Z} so that no division appears and no rounding convention is implicit. The size has been confirmed by direct enumeration at p=5,13,17p = 5, 13, 17, and the Kakeya property by exhaustive check over all nonzero directions at the smaller of those primes.

Preamble
import Definitions.Def_FiniteFieldKakeya

open Finset FiniteFieldKakeya
Formal statement
theorem FiniteFieldKakeya.exists_kakeya_card_three_dim_one_mod_four
    (p : ℕ) [Fact (Nat.Prime p)] (hp : p % 4 = 1) :
    ∃ K : Finset (Fin 3 → ZMod p), FiniteFieldKakeya.IsKakeyaSet K ∧
      (8 * K.card : ℤ) = 2 * (p : ℤ) ^ 3 + 7 * (p : ℤ) ^ 2 + 4 * (p : ℤ) - 5 := by sorry
Source
B. Georgiev, J. Gómez-Serrano, T. Tao, A. Wagner, "Mathematical exploration and discovery at scale", arXiv:2511.02864 (2025), Section 6.1; companion AlphaEvolve problem repository, Problem 1 "Kakeya and Nikodym sets in finite fields", experiment experiments/finite_field_kakeya_problem/. The construction and the p mod 4 case split are stated in that experiment's lean_proof/kakeya.lean header. CAUTION: the companion write-up deep_think_docs/kakeya2.tex is internally inconsistent, giving |K| = (2p^3+7p^2-1)/8 in its theorem statement (line 36) and (2p^3+7p^2-13)/8 at the end of its own proof (line 171); neither matches enumeration. The formula used here, (2p^3+7p^2+4p-5)/8, is the one in kakeya.lean and is the one confirmed by direct enumeration at p = 5, 13, 17. Background: Z. Dvir, JAMS 22 (2009), 1093-1097.

View graph