509 citations · 1k across the 48 of their papers we have counts for
48 papers
Large-Scale Formal Proof for the Working Mathematician -- Lessons learnt from the ALEXANDRIA Project
Lawrence C Paulson
ALEXANDRIA is an ERC-funded project that started in 2017, with the aim of bringing formal verification to mathematics. The past six years have seen great strides in the formalisati…
Mathematical Proof Between Generations
Jonas Bayer, Christoph Benzmüller, Kevin Buzzard +7
A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This…
Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
Chelsea Edmonds, Lawrence C. Paulson
The formalisation of mathematics is continuing rapidly, however combinatorics continues to present challenges to formalisation efforts, such as its reliance on techniques from a wi…
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…
Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
Lawrence C Paulson
In 1964, Paul Erdős published a paper settling a question about function spaces that he had seen in a problem book. Erdős proved that the answer was yes if and only if the continuu…
A Modular First Formalisation of Combinatorial Design Theory
Chelsea Edmonds, Lawrence Paulson
Combinatorial design theory studies set systems with certain balance and symmetry properties and has applications to computer science and elsewhere. This paper presents a modular a…