The strong cylinder conjecture asserts that, for a prime number 
, a set of 
points in the three-dimensional
affine space over the finite
field 
is a union of 
distinct parallel lines if every affine
plane meets it in a multiple of 
points (Ball et al. 2007).
Deng et al. (2026, Theorem 1.1) report a proof for every prime number 
. Sziklai (2026) gives a separate proof candidate. Deng
et al. (2026, Theorem 1.2) derive the three-dimensional case of Rédei's
factorization conjecture. If 
contain zero and every vector
is uniquely expressible as 
with 
and 
,
at least one of the two sets is contained in a plane through
zero. The authors credit AI with proof development and report a Lean formalization.
