Conway's 99-graph problem

Theorem · completeGraphIsClique

A finset of vertices in a complete graph is always a clique.

Formal statement · Lean 4.lean

lemma completeGraphIsClique (s : Finset V) : (⊤ : SimpleGraph V).IsClique s := by
  sorry

Proof. sorry

Nobody has tried yet.