Search Results

Documents authored by Brown, Chad E.

Document
DOI: 10.4230/LIPIcs.ITP.2024.16
A Formal Proof of R(4,5)=25

Authors: Thibault Gauthier and Chad E. Brown

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
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.
Cite as

Thibault Gauthier and Chad E. Brown. A Formal Proof of R(4,5)=25. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{gauthier_et_al:LIPIcs.ITP.2024.16,
  author =	{Gauthier, Thibault and Brown, Chad E.},
  title =	{{A Formal Proof of R(4,5)=25}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.16},
  URN =		{urn:nbn:de:0030-drops-207446},
  doi =		{10.4230/LIPIcs.ITP.2024.16},
  annote =	{Keywords: Ramsey numbers, SAT solvers, symmetry breaking, generalization, HOL4}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.9
Automated Theorem Proving for Metamath

Authors: Mario Carneiro, Chad E. Brown, and Josef Urban

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Metamath is a proof assistant that keeps surprising outsiders by its combination of a very minimalist design with a large library of advanced results, ranking high on the Freek Wiedijk’s 100 list. In this work, we develop several translations of the Metamath logic and its large set-theoretical library into higher-order and first-order TPTP formats for automated theorem provers (ATPs). We show that state-of-the-art ATPs can prove 68% of the Metamath problems automatically when using the premises that were used in the human-written Metamath proofs. Finally, we add proof reconstruction and premise selection methods and combine the components into the first hammer system for Metamath.
Cite as

Mario Carneiro, Chad E. Brown, and Josef Urban. Automated Theorem Proving for Metamath. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{carneiro_et_al:LIPIcs.ITP.2023.9,
  author =	{Carneiro, Mario and Brown, Chad E. and Urban, Josef},
  title =	{{Automated Theorem Proving for Metamath}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.9},
  URN =		{urn:nbn:de:0030-drops-183846},
  doi =		{10.4230/LIPIcs.ITP.2023.9},
  annote =	{Keywords: Metamath, Automated theorem proving, Interactive theorem proving, Formal proof assistants, proof discovery}
}
Document
DOI: 10.4230/OASIcs.FMBC.2022.4
Proofgold: Blockchain for Formal Methods

Authors: Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, and Josef Urban

Published in: OASIcs, Volume 105, 4th International Workshop on Formal Methods for Blockchains (FMBC 2022)

Abstract
Proofgold is a peer to peer cryptocurrency making use of formal logic. Users can publish theories and then develop a theory by publishing documents with definitions, conjectures and proofs. The blockchain records the theories and their state of development (e.g., which theorems have been proven and when). Two of the main theories are a form of classical set theory (for formalizing mathematics) and an intuitionistic theory of higher-order abstract syntax (for reasoning about syntax with binders). We have also significantly modified the open source Proofgold Core client software to create a faster, more stable and more efficient client, Proofgold Lava. Two important changes are the cryptography code and the database code, and we discuss these improvements. We also discuss how the Proofgold network can be used to support large formalization efforts.
Cite as

Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, and Josef Urban. Proofgold: Blockchain for Formal Methods. In 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, pp. 4:1-4:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{brown_et_al:OASIcs.FMBC.2022.4,
  author =	{Brown, Chad E. and Kaliszyk, Cezary and Gauthier, Thibault and Urban, Josef},
  title =	{{Proofgold: Blockchain for Formal Methods}},
  booktitle =	{4th International Workshop on Formal Methods for Blockchains (FMBC 2022)},
  pages =	{4:1--4:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-250-1},
  ISSN =	{2190-6807},
  year =	{2022},
  volume =	{105},
  editor =	{Dargaye, Zaynah and Schneidewind, Clara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2022.4},
  URN =		{urn:nbn:de:0030-drops-171851},
  doi =		{10.4230/OASIcs.FMBC.2022.4},
  annote =	{Keywords: Formal logic, Blockchain, Proofgold}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.9
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof

Authors: Chad E. Brown, Cezary Kaliszyk, and Karol Pąk

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
We formally introduce a foundation for computer verified proofs based on higher-order Tarski-Grothendieck set theory. We show that this theory has a model if a 2-inaccessible cardinal exists. This assumption is the same as the one needed for a model of plain Tarski-Grothendieck set theory. The foundation allows the co-existence of proofs based on two major competing foundations for formal proofs: higher-order logic and TG set theory. We align two co-existing Isabelle libraries, Isabelle/HOL and Isabelle/Mizar, in a single foundation in the Isabelle logical framework. We do this by defining isomorphisms between the basic concepts, including integers, functions, lists, and algebraic structures that preserve the important operations. With this we can transfer theorems proved in higher-order logic to TG set theory and vice versa. We practically show this by formally transferring Lagrange’s four-square theorem, Fermat 3-4, and other theorems between the foundations in the Isabelle framework.
Cite as

Chad E. Brown, Cezary Kaliszyk, and Karol Pąk. Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brown_et_al:LIPIcs.ITP.2019.9,
  author =	{Brown, Chad E. and Kaliszyk, Cezary and P\k{a}k, Karol},
  title =	{{Higher-Order Tarski Grothendieck as a Foundation for Formal Proof}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{9:1--9:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.9},
  URN =		{urn:nbn:de:0030-drops-110643},
  doi =		{10.4230/LIPIcs.ITP.2019.9},
  annote =	{Keywords: model, higher-order, Tarski Grothendieck, proof foundation}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact