Skip to content

Erdős problem 1098

Let GG be a group and Γ=Γ(G)\Gamma=\Gamma(G) be the non-commuting graph, with vertices the elements of GG and an edge between gg and hh if and only if gg and hh do not commute, gh≠hggh\neq hg.

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1098.lean

Retained formal statement1 of 4

Let GG be a group and Γ=Γ(G)\Gamma=\Gamma(G) be the non-commuting graph, with vertices the elements of GG and an edge between gg and hh if and only if gg and hh do not commute, gh≠hggh\neq hg.

If Γ\Gamma contains no infinite complete subgraph, then is there a finite bound on the size of complete subgraphs of Γ\Gamma?

This was solved by Neumann [Ne76], who proved that Γ\Gamma contains no infinite complete subgraph if and only if the centre of the group has finite index, and noted that if the centre has index nn then Γ\Gamma contains no complete subgraph on >n>n vertices.

FormalConjectures/ErdosProblems/1098.leanErdos1098.erdos_10984 linesExact file
True ↔  ∀ (G : Type u_1) [inst : Group G],    (∀ (s : Set G), (Erdos1098.nonCommutingGraph G).IsClique s → s.Finite) →      ∃ n, ∀ (s : Finset G), (Erdos1098.nonCommutingGraph G).IsClique ↑s → s.card ≤ n
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.