Lawrence C. Paulson

The Plünnecke-Ruzsa Inequality
by Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics
by Chelsea Edmonds and Lawrence C. Paulson

Constructing the Reals as Dedekind Cuts of Rationals
by Jacques D. Fleuriot and Lawrence C. Paulson

Ackermann's Function Is Not Primitive Recursive
by Lawrence C. Paulson

Wetzel's Problem and the Continuum Hypothesis
by Lawrence C. Paulson

Young's Inequality for Increasing Functions
by Lawrence C. Paulson

Irrational numbers from THE BOOK
by Lawrence C. Paulson

Roth's Theorem on Arithmetic Progressions
by Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

Szemerédi's Regularity Lemma
by Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

Combinatorial Design Theory
by Chelsea Edmonds and Lawrence C. Paulson

Grothendieck's Schemes in Algebraic Geometry
by Anthony Bordg, Lawrence C. Paulson and Wenda Li

Ordinal Partitions
by Lawrence C. Paulson

The Nash-Williams Partition Theorem
by Lawrence C. Paulson

Zermelo Fraenkel Set Theory in Higher-Order Logic
by Lawrence C. Paulson

Fourier Series
by Lawrence C. Paulson

The Prime Number Theorem
by Manuel Eberl and Lawrence C. Paulson

Quaternions
by Lawrence C. Paulson

An Isabelle/HOL formalisation of Green's Theorem
by Mohammad Abdulaziz and Lawrence C. Paulson

Source Coding Theorem
by Quentin Hibon and Lawrence C. Paulson

The Cartan Fixed Point Theorems
by Lawrence C. Paulson

Finite Automata in Hereditarily Finite Set Theory
by Lawrence C. Paulson

Real-Valued Special Functions: Upper and Lower Bounds
by Lawrence C. Paulson

The Hereditarily Finite Sets
by Lawrence C. Paulson

Gödel's Incompleteness Theorems
by Lawrence C. Paulson

Proving the Impossibility of Trisecting an Angle and Doubling the Cube
by Ralph Romanos and Lawrence C. Paulson

Fun With Tilings
by Tobias Nipkow and Lawrence C. Paulson