Prove2Me

Line-system form of Conway's 99-graph problem: 9999 points, 231231 lines of size 33

Open
Conway99.conway_99_triangle_system_exists

by Gabewhigham · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsdesign-theorygraph-theorystrongly-regular-graphs

Line-system (partial linear space) form of Conway's 99-graph problem.

A graph that is strongly regular with parameters (99,14,1,2)(99,14,1,2) has λ=1\lambda = 1, so every edge lies in a unique triangle and the 693693 edges are partitioned into 231231 triangles. Reading the triangles as lines, such a graph is exactly the collinearity graph of a partial linear space on 9999 points whose lines have three points each. This statement asserts the existence of that incidence structure.

Concretely, the assertion is that there is a family LL of subsets of a 9999-element point set PP (the lines) with the following four properties.

  1. Every line has exactly three points: ∣l∣=3|l| = 3 for all l∈Ll \in L.
  2. Two distinct lines meet in at most one point: ∣l1∩l2∣≤1|l_1 \cap l_2| \le 1 for distinct l1,l2∈Ll_1, l_2 \in L.
  3. Every point lies on exactly seven lines: ∣{l∈L:x∈l}∣=7|\{ l \in L : x \in l \}| = 7 for all x∈Px \in P.
  4. Any two distinct points x≠yx \ne y lying on no common line are simultaneously collinear with exactly two further points; that is,
∣{z∈P:z≠x, z≠y, (∃l∈L, x,z∈l), (∃l∈L, y,z∈l)}∣=2.\bigl|\{ z \in P : z \ne x,\ z \ne y,\ (\exists l \in L,\ x, z \in l),\ (\exists l \in L,\ y, z \in l) \}\bigr| = 2 .

Call two distinct points collinear when some line contains both, and let GG be the resulting collinearity graph. Conditions (1)-(3) make GG regular of degree 1414: the seven lines through a point xx contribute two neighbours each, and by (2) no neighbour is counted twice. Condition (4) says that two distinct non-adjacent vertices of GG have exactly two common neighbours. The remaining strong-regularity condition, that adjacent vertices have exactly one common neighbour, is not assumed here: it follows from (1)-(4) by counting the paths of length two leaving a fixed vertex. Hence the existence of such a line system is sufficient for the existence of a strongly regular graph with parameters (99,14,1,2)(99,14,1,2), and it is also necessary, the lines being the triangles of such a graph.

No such line system is known, and none is known not to exist; the statement carries the full open content of Conway's 99-graph problem.

Preamble
import Mathlib.Combinatorics.SimpleGraph.StronglyRegular

open Finset
Formal statement
namespace Conway99

theorem conway_99_triangle_system_exists :
    ∃ L : Finset (Finset (Fin 99)),
      (∀ l ∈ L, l.card = 3) ∧
      (∀ l₁ ∈ L, ∀ l₂ ∈ L, l₁ ≠ l₂ → (l₁ ∩ l₂).card ≤ 1) ∧
      (∀ x : Fin 99, (L.filter fun l => x ∈ l).card = 7) ∧
      (∀ x y : Fin 99, x ≠ y → (∀ l ∈ L, ¬(x ∈ l ∧ y ∈ l)) →
        (univ.filter fun z : Fin 99 => z ≠ x ∧ z ≠ y ∧
            (∃ l ∈ L, x ∈ l ∧ z ∈ l) ∧ (∃ l ∈ L, y ∈ l ∧ z ∈ l)).card = 2) := by sorry

end Conway99
Source
J. H. Conway, 'Five $1,000 Problems (Update 2017)', OEIS, https://oeis.org/A248380/a248380.pdf (Problem 1). The partial-linear-space reformulation (a (99,14,1,2) graph has every edge in a unique triangle, so its 693 edges split into 231 triangles of a partial linear space on 99 points with 7 lines through each point) is the standard one, see https://en.wikipedia.org/wiki/Conway%27s_99-graph_problem and the mission milestone Conway99.conway_99_cliqueFinset_three_card.

View graph