Towards Closing the Trust Gap in the SAT Certification of Ramsey Numbers R(3,8) and R(3,9)

4 SimpleGraph

Lemma 16 induce_compl
✓
#

Lean declarations

Proof ▶
Theorem 17 IsIndepSet.subset
✓
#

Lean declarations

Proof ▶
Theorem 18 Iso.isNIndepSet_one
✓
#

Lean declarations

Proof ▶
Lemma 19 Iso.IsClique
✓
#

Lean declarations

Proof ▶
Lemma 20 Iso.IsIndepSet
✓
#

Lean declarations

Proof ▶
Lemma 21 Iso.IsNClique
✓
#

Uses

Lean declarations

Proof ▶
Lemma 22 Iso.IsNIndepSet
✓
#

Uses

Lean declarations

Proof ▶
Lemma 23 Iso.cliqueNum
✓
#

Uses

Lean declarations

Proof ▶
Lemma 24 Iso.indepNum
✓
#

Uses

Lean declarations

Proof ▶
Definition 25 Iso.compl
✓
#

Lean declarations

Lemma 26 fintype_cliqueNum_bddAbove
✓
#

Lean declarations

Proof ▶
Lemma 27 fintype_indepNum_bddAbove
✓
#

Lean declarations

Proof ▶
Lemma 28 cliqueNum_pos
✓
#

Uses

Lean declarations

Proof ▶
Lemma 29 indepNum_pos
✓
#

Uses

Lean declarations

Proof ▶
Lemma 30 cliqueNum_top
✓
#

Lean declarations

Proof ▶
Lemma 31 cliqueNum_bot
✓
#

Uses

Lean declarations

Proof ▶
Lemma 32 indepNum_bot
✓
#

Uses

Lean declarations

Proof ▶
Lemma 33 indepNum_top
✓
#

Uses

Lean declarations

Proof ▶
Lemma 34 exists_isNClique_of_le_cliqueNum
✓
#

Lean declarations

Proof ▶
Lemma 35 exists_isNIndset_of_le_indepNum
✓
#

Lean declarations

Proof ▶
Lemma 36 cliqueNum_lt_iff_cliqueFree
✓
#

Uses

Lean declarations

Proof ▶
Lemma 37 Embedding.indepNum_mono
✓
#

Uses

Lean declarations

Proof ▶
Lemma 38 Embedding.cliqueNum_mono
✓
#

Uses

Lean declarations

Proof ▶