A Formal Proof of R(4,5)=25
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F24%3A00380284" target="_blank" >RIV/68407700:21730/24:00380284 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.4230/LIPIcs.ITP.2024.16" target="_blank" >https://doi.org/10.4230/LIPIcs.ITP.2024.16</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.4230/LIPIcs.ITP.2024.16" target="_blank" >10.4230/LIPIcs.ITP.2024.16</a>
Alternative languages
Result language
angličtina
Original language name
A Formal Proof of R(4,5)=25
Original language description
In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The authors have performed the computational parts of the proof with different implementations in order to reduce the possibility of an error in their programs. In this work, we prove this theorem in the interactive theorem prover HOL4 limiting the uncertainty to the small HOL4 kernel. Instead of verifying their algorithms directly, we rely on the HOL4 interface to MiniSat to prove gluing lemmas. To reduce the number of such lemmas and thus make the computational part of the proof feasible, we implement a generalization algorithm. We verify that its output covers all the possible cases by implementing a custom SAT-solver extended with a graph isomorphism checker.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/LL1902" target="_blank" >LL1902: Powering SMT Solvers by Machine Learning</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2024
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
15th International Conference on Interactive Theorem Proving (ITP 2024), Proceeding
ISBN
978-3-95977-337-9
ISSN
1868-8969
e-ISSN
—
Number of pages
18
Pages from-to
—
Publisher name
Schloss Dagstuhl International Conference and Research Center for Computer Sci.
Place of publication
Dagstuhl
Event location
Tbilisi
Event date
Sep 9, 2024
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—