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

5 Inequalities

Lemma 39 Fin.val_three

✓

#

Proof ▶

Lemma 40 \(σ\)_helper

✓

#

Proof ▶

Lemma 41 \(s_i\)_vanish

✓

#

Proof ▶

Theorem 42 R36ub

✓

#

Theorem 43 R36

✓

#

Proof ▶

Theorem 44 R37ub

✓

#

Theorem 45 R37

✓

#

Proof ▶

Theorem 46 \(e 3 6 11 ≥ 11\)

✓

#

Theorem 47 \(e 3 6 12 ≥ 15\)

✓

#

Theorem 48 \(e 3 6 13 ≥ 20\)

✓

#

Theorem 49 \(e 3 6 14 ≥ 15\)

✓

#

Theorem 50 \(e 3 6 15 ≥ 32\)

✓

#

Theorem 51 \(e 3 6 16 ≥ 50\)

✓

#

Lemma 52 R38lb

✓

#

Proof ▶

Lemma 53 \(e 3 7 18 ≥ 36\)

✓

#

Proof ▶

Theorem 54 \(e 3 7 19 ≥ 44\)

✓

#

Lemma 55 \(e 3 7 20 ≥ 50\)

✓

#

Proof ▶

Lemma 56 \(e 3 7 21 ≥ 59\)

✓

#

Proof ▶

Lemma 57 \(e 3 7 21 ≥ 59\)

✓

#

Proof ▶

Theorem 58 Graver’s Ineq 9: \(e 3 8 26 ≥ 80\)

✓

#

Proof ▶

Theorem 59 Graver’s Ineq 9: \(e 3 8 26 ≥ 80\)

✓

#

Proof ▶

Theorem 60 Graver’s Ineq 10: \(e 3 8 27 ≥ 88\)

✓

#

Proof ▶

Theorem 61 Graver’s Ineq 11: \(e 3 8 28 ≥ 99\)

✓

#

Proof ▶

Lemma 62 Gregular_of_isXY

✓

#

Proof ▶

Theorem 63 R39Ineq

✓

#

Proof ▶

Theorem 64 R39_36_graph_IsRegular8

✓

#

Proof ▶

Theorem 65 R39_36_graph_has_R38_27

✓

#

Proof ▶