5 citations · 6 across the 5 of their papers we have counts for
5 papers
A Formalisation of a Special Case of the Union-Closed Conjecture in Isabelle/HOL
Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
A 2021 proof of a special case of the Union-Closed Conjecture, by Aaronson, Ellis and Leader, has been formalised in the proof assistant Isabelle/HOL. Our discussion involves sketc…
Towards a Common Framework for Autoformalization
Agnieszka Mensfelt, David Tena Cucala, Santiago Franco +3
Autoformalization has emerged as a term referring to the automation of formalization - specifically, the formalization of mathematics using interactive theorem provers (proof assis…
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL
Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
We have formalised Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions, two major results in extremal graph theory and additive combinatorics, using the proo…
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson
We give an overview of our formalizations in the proof assistant Isabelle/HOL of certain irrationality and transcendence criteria for infinite series from three different research…
Formalising Ordinal Partition Relations Using Isabelle/HOL
Mirna Džamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
This is an overview of a formalisation project in the proof assistant Isabelle/HOL of a number of research results in infinitary combinatorics and set theory (more specifically in…