3 Search Results for "Koutsoukou-Argyraki, Angeliki"

Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2025.38
Sledgehammering Without ATPs (Short Paper)

Authors: Martin Desharnais and Jasmin Blanchette

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We describe an alternative architecture for "hammers," inspired by Magnushammer, in which proofs are found by the proof assistant’s built-in automation instead of by external automatic theorem provers (ATPs). We implemented this approach in Isabelle’s Sledgehammer and evaluated it. The new ATP-free approach nicely complements the traditional Sledgehammer. The two approaches in combination solve more goals than the traditional ATP-based approach alone.
Cite as

Martin Desharnais and Jasmin Blanchette. Sledgehammering Without ATPs (Short Paper). In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 38:1-38:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.ITP.2025.38,
  author =	{Desharnais, Martin and Blanchette, Jasmin},
  title =	{{Sledgehammering Without ATPs}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{38:1--38:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.38},
  URN =		{urn:nbn:de:0030-drops-246366},
  doi =		{10.4230/LIPIcs.ITP.2025.38},
  annote =	{Keywords: Interactive theorem proving, proof assistants, proof automation}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.18
Formalising New Mathematics in Isabelle: Diagonal Ramsey

Authors: Lawrence C. Paulson

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
The formalisation of mathematics is becoming routine, but its value to research mathematicians remains unproven. There are few examples of using proof assistants to verify new work. This paper reports the formalisation - inspired by a Lean one by Bhavik Mehta - of a major new result [Marcelo Campos et al., 2023] about Ramsey numbers. One unexpected finding was a heavy role for computer algebra techniques.
Cite as

Lawrence C. Paulson. Formalising New Mathematics in Isabelle: Diagonal Ramsey. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{paulson:LIPIcs.ITP.2025.18,
  author =	{Paulson, Lawrence C.},
  title =	{{Formalising New Mathematics in Isabelle: Diagonal Ramsey}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.18},
  URN =		{urn:nbn:de:0030-drops-246163},
  doi =		{10.4230/LIPIcs.ITP.2025.18},
  annote =	{Keywords: Isabelle, formalisation of mathematics, Ramsey’s theorem, computer algebra}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ITP.2023.1
Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk)

Authors: Angeliki Koutsoukou-Argyraki

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

Abstract
In this talk, I will present an overview of recent formalisations, in the interactive theorem prover Isabelle/HOL, of significant theorems in additive combinatorics, an area of combinatorial number theory. The formalisations of these theorems were the first in any proof assistant to my knowledge. For each of these theorems, I will discuss selected aspects of the formalisation process, focussing on observations on our treatment of certain mathematical arguments when translated into Isabelle/HOL and our overall formalisation experience with Isabelle/HOL for this area of mathematics.
Cite as

Angeliki Koutsoukou-Argyraki. Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{koutsoukouargyraki:LIPIcs.ITP.2023.1,
  author =	{Koutsoukou-Argyraki, Angeliki},
  title =	{{Formalisation of Additive Combinatorics in Isabelle/HOL}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{1:1--1:2},
  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.1},
  URN =		{urn:nbn:de:0030-drops-183760},
  doi =		{10.4230/LIPIcs.ITP.2023.1},
  annote =	{Keywords: Additive combinatorics, additive number theory, combinatorial number theory, formalisation of mathematics, interactive theorem proving, proof assistants, Isabelle/HOL}
}
  • Refine by Type
  • 3 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 1 2023

  • Refine by Author
  • 1 Blanchette, Jasmin
  • 1 Desharnais, Martin
  • 1 Koutsoukou-Argyraki, Angeliki
  • 1 Paulson, Lawrence C.

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Logic and verification
  • 2 Mathematics of computing → Combinatorics
  • 1 Computing methodologies → Symbolic and algebraic manipulation
  • 1 Computing methodologies → Theorem proving algorithms
  • 1 Theory of computation → Automated reasoning

  • Refine by Keyword
  • 2 formalisation of mathematics
  • 2 proof assistants
  • 1 Additive combinatorics
  • 1 Interactive theorem proving
  • 1 Isabelle
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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