Maximally symmetric $(23_4)$ configurations and the end of the existence problem for geometric $(n_4)$ configurations
Wenhao Lu
math.CO
Oct 8, 2026 · v1
cs.CG cs.DM
TL;DR
The incidence checks for both (23_4) configurations, one over the integers and one over Q(√17), are formalized in Lean 4.
Abstract
A geometric $(n_4)$ configuration is a set of $n$ points and $n$ lines in the real projective plane such that every point lies on exactly four of the lines and every line contains exactly four of the points. The question of which $n$ admit such a configuration was posed by Grünbaum in 2000, following his 1990 paper with Rigby that gave the first geometric $4$-configuration, a $(21_4)$. Successive work of Bokowski-Schewe, of Bokowski, Grünbaum and Schewe, of Bokowski-Pilaud, and of Cuntz settled every case but one. Cuntz's 2018 paper, which constructed $(22_4)$ and $(26_4)$ configurations, states that only $n=23$ remained open. We settle this last case. We prove that for every prime $n\equiv3\pmod4$, in particular for $n=23$, the group of projective symmetries of a geometric $(n_4)$ configuration has order at most four, which explains why $n=23$ resisted the symmetric constructions that settled the other values. Reducing the case of a Klein four-group of symmetries to a few thousand bilinear polynomial systems in $18$ unknowns, and solving all of them exactly with Gröbner bases and saturation, we show that exactly two geometric $(23_4)$ configurations reach this bound, up to projective equivalence, and that there are no others even over $\mathbb{C}$. Both are self-polar with respect to a conic. The first has integer homogeneous coordinates; the second is defined over $\mathbb{Q}(\sqrt{17})$, but not over $\mathbb{Q}$. Consequently geometric $(n_4)$ configurations exist if and only if $n\ge18$ and $n\ne19$. A third configuration, self-polar and defined over a real cubic field, has only a single symmetry of order two. The same classification at $n=22$ and $n=26$ recovers Cuntz's configurations and finds three new combinatorial types at $n=22$ and $94$ at $n=26$, among them a $(26_4)$ configuration that is self-polar with respect to a conic without real points.
Problem
Grünbaum asked for which n a geometric (n_4) configuration of points and lines in the real projective plane exists. Prior work settled every case except n=23.
Approach
The authors prove that for primes n≡3 (mod 4) the projective symmetry group of an (n_4) configuration has order at most four. They reduce the Klein four-group case to a few thousand bilinear polynomial systems in 18 unknowns and solve them exactly with Gröbner bases and saturation. A finite-field CP-SAT search provided an initial candidate. The resulting incidence checks were verified by hand, by Python scripts, and in Lean 4.
Results
Exactly two Klein-symmetric geometric (23_4) configurations exist up to projective equivalence: one integral and one over Q(√17). Both are self-polar. Hence geometric (n_4) configurations exist if and only if n≥18 and n≠19. The same classification yields three new combinatorial types at n=22 and 94 at n=26.