Papers With

← All papers
First page of The strong cylinder conjecture and Rédei's factorization conjecture in three dimensions

The strong cylinder conjecture and Rédei's factorization conjecture in three dimensions

Haihua Deng, Weicong Li, Weiye Zhang

math.CO Nov 8, 2026 · v1
formalization combinatorics geometry
Read PDF arXiv abstract Code
TL;DR
The authors formalized the paper's results in Lean 4 with AI assistance and released the formalization in a public GitHub repository.
Abstract
In this paper, we prove the strong cylinder conjecture, that is, for every prime $p$, a set of $p^2$ points in $\mathbb F_p^3$ that meets every affine plane in a multiple of $p$ points is a union of $p$ distinct parallel affine lines. We use this result to resolve Rédei's 1970 factorization conjecture in three dimensions: if $A,B\subseteq\mathbb F_p^3$ contain zero and every vector in $\mathbb F_p^3$ has a unique expression $a+b$ with $a\in A$ and $b\in B$, then one of the two sets is contained in a plane through zero.
Problem

The strong cylinder conjecture asks whether every set of p^2 points in F_p^3 meeting each affine plane in a multiple of p points is a union of p parallel affine lines. Rédei's 1970 conjecture asks whether, in a normalized factorization A⊕B=F_p^3, one factor must lie in a plane through zero. Rédei's conjecture had previously been verified only for p ≤ 13.

Approach

The proof assumes a counterexample for p ≥ 11, since small primes were settled earlier. It studies the projective dual configuration of white and black points and shows that all plane intersections have size 0, p, or 2p. Projection moments are interpolated through linear and quadratic forms, using complete intersections and duality for evaluation relations. A classification of generalized hyperfocused arcs then rules out a quadric containing the white point set, which yields a contradiction. Rédei's conjecture follows from p-divisibility of the larger factor, power sums of linear forms, and Rédei's planar factorization theorem. The authors used OpenAI GPT-6 Astra to help develop the proofs and write Lean 4 formalizations, which are available on GitHub.

Results

The strong cylinder conjecture is proved for every prime p. As a consequence, Rédei's factorization conjecture holds in three dimensions: in every normalized factorization of F_p^3, one factor is contained in a plane through zero.