A -graph has exactly triangles
ProvedConway99.conway_99_cliqueFinset_three_cardcombinatoricsgraph-theorystrongly-regular-graphs
Any strongly regular graph with parameters contains exactly triangles, where a triangle is a -element clique.
Since , every edge lies in exactly one triangle, and every triangle contains three edges, so the number of triangles is ; equivalently . A hypothetical -graph is therefore a partial linear space with points and lines of size , each point on lines.
Preamble
import Mathlib.Combinatorics.SimpleGraph.StronglyRegular import Mathlib.Combinatorics.SimpleGraph.Clique open SimpleGraph
Formal statement
namespace Conway99
theorem conway_99_cliqueFinset_three_card {V : Type*} [Fintype V] [DecidableEq V]
{g : SimpleGraph V} [DecidableRel g.Adj] (h : g.IsSRGWith 99 14 1 2) :
(g.cliqueFinset 3).card = 231 := by sorry
end Conway99Source
Triangle count from lambda = 1 for the parameters of Conway's 99-graph problem; https://en.wikipedia.org/wiki/Conway%27s_99-graph_problem
Human review
Confirmed by the mission captain (proposal self-audit).