AWESOME AI PROOFS
← Problems
Research / Sep 1, 2026

Kourovka 21.29: Common neighbours in generalized Saxl graphs

Do every two vertices in the relevant generalized Saxl graph of a primitive permutation group have a common neighbour?

Model / AI: Codex, ChatGPT Pro, Claude

machine-checked (every-base-size counterexamples)self-reported (every-base-size counterexamples)
Sep 1, 2026

Infinite counterexample families

Model / AI: Codex, ChatGPT Pro, Claude

machine-checked (every-base-size counterexamples)self-reported (every-base-size counterexamples)

Rizzoli and Thomas used several models to find and develop primitive-group counterexamples for every base size, answering Kourovka Problem 21.29 negatively. Codex produced much of the computational code and most of the Lean formalization, while the authors reviewed statements and the completed formalization.

Source read 2026-09-08. Read the paper abstract and the linked public source record. The Lean project was not rebuilt and specialist review was not found.