graph_automorphism_prime
Disprovedgraph-theorynumber-theory
Graph automorphism conjecture: For prime n, every automorphism of a connected n-vertex graph has order dividing n. Related to Cayley's theorem. Special cases proved; general conjecture open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem graph_automorphism_prime (n : ℕ) (hn : 2 ≤ n) (hp : Nat.Prime n)
(G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
(hconn : G.Connected) :
∀ phi : Equiv.Perm (Fin n),
(∀ v w : Fin n, G.Adj v w ↔ G.Adj (phi v) (phi w)) →
phi ^ n = Equiv.refl (Fin n) := by
sorrySource