Editing Ramsey's theorem (section)

=== Formal verification of Ramsey numbers ===

The Ramsey number <math>R(3,8)</math> and <math>R(3,9)</math> have been formally verified to be 28 and 36.<ref>{{cite arXiv |last1=Li |first1=Zhengyu |last2=Duggan |first2=Conor |last3=Bright |first3=Curtis |last4=Ganesh |first4=Vijay |title=Verified Certificates via SAT and Computer Algebra Systems for the Ramsey R(3, 8) and R(3, 9) Problems |date=2025 |class=cs.LO |eprint=2502.06055}}</ref> This verification was achieved using a combination of Boolean satisfiability (SAT) solving and computer algebra systems (CAS). The proof was generated automatically using the [https://uwaterloo.ca/mathcheck/ SAT+CAS] approach, marking the first certifiable proof of <math>R(3,8) = 28</math> and <math>R(3,9)=36</math>. The verification process for <math>R(3,8)</math> and <math>R(3,9)</math> was conducted using the SAT+CAS framework MathCheck, which integrates a SAT solver with a computer algebra system. The verification for <math>R(3,8) = 28</math> was completed in approximately 8 hours of wall clock time, producing a total proof size of 5.8 GiB. The verification for <math>R(3,9) = 36</math> was significantly more computationally intensive, requiring 26 hours of wall clock time and generating 289 GiB of proof data. The correctness of these results was independently verified using a modified version of the [https://www.cs.utexas.edu/~marijn/drat-trim/ DRAT-trim] proof checker.<ref>{{cite arXiv |last1=Li |first1=Zhengyu |last2=Duggan |first2=Conor |last3=Bright |first3=Curtis |last4=Ganesh |first4=Vijay |title=Verified Certificates via SAT and Computer Algebra Systems for the Ramsey R(3, 8) and R(3, 9) Problems |date=2025 |class=cs.LO |eprint=2502.06055}}</ref>

The Ramsey number <math>R(4,5)</math> has been formally verified to be 25.<ref>{{cite arXiv |last1=Gauthier |first1=Thibault |last2=Brown |first2=Chad E |title=A formal proof of R(4,5)=25 |date=2024 |class=cs.LO |eprint=2404.01761}}</ref> The original proof, developed by McKay and Radziszowski in 1995, combined high-level mathematical arguments with computational steps and used multiple independent implementations to reduce the possibility of programming errors. The formal proof was carried out using the [[HOL (proof assistant)|HOL4]] interactive theorem prover, limiting the potential for errors to the HOL4 kernel. Rather than directly verifying the original algorithms, the authors utilized HOL4's interface to the MiniSat SAT solver to formally prove key gluing lemmas.