A Formal Proof of R(4,5)=25

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

A Formal Proof of R(4,5)=25

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

A Formal Proof of R(4,5)=25

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/LL1902" target="_blank" >LL1902: Obohacování SMT řešičů pomocí strojového učení</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2024

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

15th International Conference on Interactive Theorem Proving (ITP 2024), Proceeding

ISBN

978-3-95977-337-9

ISSN

1868-8969

e-ISSN

—

Počet stran výsledku

18

Strana od-do

—

Název nakladatele

Schloss Dagstuhl International Conference and Research Center for Computer Sci.

Místo vydání

Dagstuhl

Místo konání akce

Tbilisi

Datum konání akce

9. 9. 2024

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—