Erdős problem 1098

Let $G$ be a group and $\Gamma=\Gamma(G)$ be the non-commuting graph, with vertices the elements of $G$ and an edge between $g$ and $h$ if and only if $g$ and $h$ do not commute, $gh\neq hg$ .

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1098.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1098.leanErdos1098.erdos_10984 linesExact file

1True ↔2  ∀ (G : Type u_1) [inst : Group G],3    (∀ (s : Set G), (Erdos1098.nonCommutingGraph G).IsClique s → s.Finite) →4      ∃ 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.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:1098
PLBY Lean proofsErdosProblems.Erdos1098

Reported activity

Reported by these sources. Not reviewed here.

Formalization
Erdős AI contributions wiki · 25 Apr, 2026
Machine
Aristotle
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry