Towards Closing the Trust Gap in the SAT Certification of Ramsey Numbers R(3,8) and R(3,9)
1
Introduction
2
Sym2
3
Bron–Kerbosch Algorithm
4
SimpleGraph
5
Inequalities
6
Ramsey Theory
Dependency graph
2 Sym2
Definition
1
decBall
✓
#
L∃∀N
Lean declarations
Sym2.decBall
Definition
2
decBex
✓
#
L∃∀N
Lean declarations
Sym2.decBex
Definition
3
toOrderedPair
✓
#
L∃∀N
Lean declarations
Sym2.toOrderedPair
Lemma
4
exists_mem_pair
✓
#
L∃∀N
Lean declarations
Sym2.exists_mem_pair
Proof
▶
Lemma
5
toOrderedPair_repr
✓
#
Uses
Definition 3
L∃∀N
Lean declarations
Sym2.toOrderedPair_repr
Proof
▶
Lemma
6
toOrderedPair_inj
✓
#
Uses
Definition 3
Lemma 5
L∃∀N
Lean declarations
Sym2.toOrderedPair_inj
Proof
▶
Lemma
7
toOrderedPair_IsDiag_of_eq
✓
#
Uses
Definition 3
L∃∀N
Lean declarations
Sym2.toOrderedPair_IsDiag_of_eq
Proof
▶
Lemma
8
isDiag_of_subsingleton
✓
#
L∃∀N
Lean declarations
Sym2.isDiag_of_subsingleton
Proof
▶