Common neighbour conjectures for Saxl graphs fail at every base size
Primitive permutation groups are constructed whose generalised Saxl graphs contain two nonadjacent vertices with no common neighbour, disproving the Burness-Giudici conjecture and its extension at every base size.
- Lab
- Independent
- Model
- Codex; ChatGPT Pro; Claude
- Field
- Mathematics
- Date
- 2026-09-01
- Human collaborators
- Aluna Rizzoli, Adam R. Thomas
- Problem posed
- 2020 · open 6 yrs
Sources
Original work
Independent commentary
What was found
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 to arbitrary base size. Both are disproved: for each integer B at least 2 the paper constructs infinitely many primitive groups of base size B whose generalised Saxl graphs contain two nonadjacent vertices with no common neighbour. At base size two there are 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, and in the affine and product families the Saxl graphs have diameter exactly three. The result also answers Problem 21.29 of the Kourovka Notebook.
Novelty check
Both conjectures are named, attributed and dated in the paper: Burness and Giudici for base size two in 2020, and Freedman, Huang, Lee and Rekvényi for the extension to arbitrary base size. The counterexamples are exhibited as explicit infinite families rather than existence claims, and their spread across three of the five O'Nan-Scott types is stated precisely. The Kourovka Notebook problem answered here is 21.29, which is not among the eight problems covered by this registry's existing Kourovka entry. No prior counterexample appears.
Caveats and known objections
A preprint days old at entry, unrefereed, with no independent human check on record. The formal grade rests on Theorem 1.2, the statement that counterexamples exist at every base size, which is verified in Lean 4 with no sorry placeholders and no project-specific axioms, with the source in the paper's repository; the three additional base-size-two families and the diameter computations are not covered by that formalization, and the Lean statements have not been audited by a third party against the paper. Autonomy is graded collaborative on a detailed disclosure describing back-and-forth rather than handoff: the project began with Codex support aimed at proving the conjecture for soluble affine groups, the authors then worked with Codex, ChatGPT Pro and Claude to find further examples and constructions, search the literature and draft the manuscript, Codex implemented much of the Magma, GAP, Python and C++ code, and the Lean formalisation was produced primarily by Codex with the authors reviewing its theorem statements and verifying the completed formalisation.
Also recorded at
vibemathedcommon-neighbour-conjectures-for-saxl-graphs
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and Collaborative.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and collaborative for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Common neighbour conjectures for Saxl graphs fail at every base size. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-01-saxl-common-neighbourBibTeX
@misc{whataifound-independent-2026-neighbour,
title = {Common neighbour conjectures for Saxl graphs fail at every base size},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Formally verified. Autonomy: Collaborative.},
url = {https://whataifound.org/finding/2026-09-01-saxl-common-neighbour}
}