Common Neighbour Conjectures for Saxl Graphs
For a finite permutation group, a base is a set of points with trivial pointwise stabiliser, and the generalised Saxl graph records which pairs of points lie together in a base of minimum size. Burness and Giudici conjectured that any two vertices of the Saxl graph of a primitive group of base size two have a common neighbour, and Freedman, Huang, Lee and Rekvényi extended this conjecture to arbitrary base size. We disprove both. For each integer we construct infinitely many primitive groups of base size whose generalised Saxl graphs contain two nonadjacent vertices with no common neighbour. At base size two, where this is the usual Saxl graph, we obtain three further infinite families, one each of affine, product and twisted wreath type, so the conjecture fails in three of the five O’Nan–Scott types; in the affine and product type families the Saxl graphs have diameter exactly three. This answers Problem 21.29 in the Kourovka Notebook in the negative. In the positive direction, we prove the Burness–Giudici conjecture for every primitive affine group whose point stabiliser is almost quasisimple of sporadic type, completing work of Lee and Popiel.
- Result
- Disproved(see note)
- Status
- Resolved
- AI contribution
- AI co-developed
- Method
- Computation
- Field
- Group theory
- Posed by
- Timothy Burness and Michael Giudici
- Year posed
- 2020
- Years open
- 6y
- Solved
- 2026-09-01
- Model
- ChatGPT Pro; Claude
- Vendor
- OpenAI; Anthropic
- Collaborators
- Aluna Rizzoli, Adam R. Thomas
- Verification
- Unreviewed
- Publication
- Preprint
- Significance
- 18 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
The paper disproves both the Burness–Giudici common neighbour conjecture for primitive groups of base size and its later generalisation to arbitrary base size. For every integer , it constructs infinitely many primitive permutation groups of base size whose generalised Saxl graphs contain two nonadjacent vertices with no common neighbour. At base size , it gives infinite counterexample families of affine, product and twisted wreath type, so the conjecture fails in three of the five O'Nan–Scott types.
What the AI did
The project began with Codex assisting an attempted proof and Lean formalisation of the common neighbour conjecture for soluble affine groups. A falsification search instead found counterexamples. The authors then worked with Codex, ChatGPT Pro and Claude to discover further examples and constructions, search the literature, and draft and revise the paper. Codex implemented and debugged much of the Magma, GAP, Python and C++ code and produced most of the Lean formalisation.
Verification
Unreviewed: a preprint two days old with no independent check. The counterexamples are explicit groups, so they are checkable directly by anyone with Magma or GAP, and the paper's Lean 4 formalisation of Theorem 1.2 reports no ; neither has been rebuilt here.
Source
- PaperarXiv
Submitted by VibeGene on