-
Law of quadratic reciprocity (part 2): HOL Light
A proof assistant, or theorem prover, is a computer program that checks a mathematical proof for correctness and in some cases generates a proof, or useful steps toward a proof, by itself. In a previous post, we explored how the proof of the Law of Quadratic Reciprocity (henceforth referred to as QR) can be formalised and checked for correctness…
-
When do two injections make a bijection?
On some proofs of the Schroeder-Bernstein theorem. A version of this article originally appeared in The Oxford Invariants Society magazine The Invariant in Trinity Term 2015. 1. Motivation: Sets, sizes and injections How do we know whether two sets are the same size, in other words, that they have the same number of elements? For small, finite…
-
Mathematical foundations of classical ballet
A version of this article originally appeared in The Oxford Invariants Society magazine The Invariant in Hilary Term 2016. Everyone knows that music and mathematics go well together. There are myriad examples of this, from Albert Einstein, who loved to play the violin, to John F. Nash, who listened to Bach and Mozart while solving mathematical problems.…
-
Law of quadratic reciprocity (part 1): Mizar
In the article “Formal proof—getting started” [2007a], Freek Wiedijk introduces the practical use of formal proof assistants. He shows how two contrasting programs, Mizar and HOL Light, can be used to formalise and check an elementary number theoretic proof of the Law of Quadratic Reciprocity. Mizar has a declarative proof style, whilst HOL Light is a procedural system.…
-
Proof assistants: A brief exposition
What’s the big deal about proof assistants? Why would anyone bother to write an article about them? These are good questions. In this post, I will try to answer them. A proof assistant is a computer program that checks a mathematical proof for correctness. In order for this to happen, the proof must be formalised, that…