Patrick Stevens

Former mathematics student at the University of Cambridge; now a software engineer.

All Posts

2018

Dependent types overview

Proving things in Agda, part 1: what is dependent typing?

2017

Proof of Cauchy-Schwarz

This is just a link to a beautiful proof of the Cauchy-Schwarz inequality. There are a number of elegant proofs, but this is by far my favourite, because (as...

2016

A Free Market

Martin was walking through the farmers’ market. He had scored off nearly everything on his shopping list, but one item stubbornly remained: he needed some ka...

Be a Beginner

TL;DR: Being a beginner at something is great, especially if it’s something that humans are built for.

Part III essay

Now that my time in Part III is over, I feel justified in releasing my essay, which is on the subject of Non-standard Analysis. It was supervised by Dr Thoma...

The use of jargon

I was recently having a late-night argument with someone about the following thesis:

Finitistic reducibility

There is a Hacker News thread at the moment about an article on Quanta which describes a paper which claims to prove that Ramsey’s theorem for pairs is finit...

Tennenbaum's theorem

Most recent exposition: an article on Tennenbaum’s Theorem. Comments welcome. The proof is cribbed from Dr Thomas Forster, but his notes only sketched the fa...

Modular machines

I’ve written a blurb about what a modular machine is (namely, another Turing-equivalent form of computing machine), and how a Turing machine may be simulated...

Independence of the Axiom of Choice (for programmers)

So you’ve heard that the Axiom of Choice is magical and special and unprovable and independent of set theory, and you’re here to work out what that means. Le...

Another Monty Hall explanation

Recall the Monty Hall problem: the host, Monty Hall, shows you three doors: A, B and C. You are assured that behind one of the doors is a car, and behind the...

Clojure and Exercism

I’ve been trying to learn Clojure (a LISP) through Exercism, a programming exercises tool. It took me an hour to get Hello, World! up and running, so I thoug...

How to make a life decision

This post is incomplete.

Friedberg-Muchnik theorem

Another short post to point out my new article on the Friedberg-Muchnik theorem, a theorem from computability theory. It uses what is known officially as a f...

Representable functors

Just a post to draw attention to my new article about representable functors and their links to adjoint functors. It’s very short, but it gives a reason for ...

Multiplicative determinant

I’m clearing out my desktop again, and found this document on the multiplicativity of the determinant, which I wrote in 2014. It might as well be up here.

2015

Monadicity Theorems

Another short post to highlight the existence of an article about the Monadicity Theorems, in which I prove one direction of both the Crude and Precise versi...

General Adjoint Functor Theorem

Just a post to draw attention to my new article about the General Adjoint Functor Theorem. It’s a motivation of the GAFT and its proof. I’ve never seen it mo...

My First Forcing

In the Part III Topics in Set Theory course, we have used forcing to show the consistency of the Continuum Hypothesis, and we are about to show the consisten...

Eilenberg-Moore

During my attempts to understand the fearsomely difficult Part III course “Introduction to Category Theory” by PT Johnstone, I came across the monadicity of ...

Heyting algebras

Now that we’ve had the definition of an exponential, we move on to the Heyting algebra, pages 129 through 131 of Awodey. This is still in the “exponentials” ...

Limits exercises

These are located on pages 114 through 118 of Awodey.

Exponentials in category theory

Now we come to Chapter 6 of Awodey, on exponentials, pages 119 through 128. Supposedly, this represents a kind of universal property which is not of the form...

Lottery odds

It has been proposed to me that if one is to play the National Lottery, one should be sure to select one’s own numbers instead of allowing the machine to sel...

Properties of categorical limits

We’ve seen how limits are formed, and that they exist iff products and equalisers do. Now we get to see about continuous functions and colimits, pages 105 th...

Limits and pullbacks 2

We have just had the definition of a pullback; now in Awodey pages 95 through 100 we’ll see some more about them, and after that we’ll get the more general u...

Limits and pullbacks

I’m going to skip pages 85 through 88 of Awodey for the moment, because time is starting to get short and I want to make sure I’m doing stuff which is releva...

Groups in categories

I go into this chapter hoping that it will be on things I already know about group theory. This post will be on pages 75 through 85 of Awodey.

Duality exercises

Exercise 1 is easy: at the end of Chapter 2 the corresponding products statement was proved, and the obvious dual statement turns out to be this one.

Equalisers

This is pages 62 through 71 of Awodey, on equalisers and coequalisers.

Duality in category theory

I don’t have strong preconceptions about this chapter. The previous chapter I knew would contain general constructions, and I was looking forwards to that, b...

Hom-sets and exercises

This is on pages 48 through 52 of Awodey, covering the hom-sets section and the exercises at the end of Chapter 2. Only eight more chapters after this, and I...

Products in category theory

This is on pages 38 through 48 of Awodey. I’ve been looking forward to it, because products are things which come up all over the place and I’d heard that th...

Initial, terminal, and generalised elements

This is pages 33 to 38 of Awodey.

Epis and monos

This post is on pages 29 through 33 of Awodey. It took me a while to do this, because I was basically on holiday for the past week.

Proof by contradiction

Here I explain proof by contradiction so that anyone who has ever done a sudoku and seen algebra may understand it.

Free categories and foundations

Here, I will be going through the Free Categories and Foundations sections of Awodey’s Category Theory - pages 18 through 25.

New categories from old

Here, I will be going through the Isomorphisms and Constructions sections of Awodey’s Category Theory - pages 12 through 17.

What is a Category?

This post will cover the initial “examples” section of Category Theory. Because there aren’t really very deep concepts in this section, this is probably a le...

Category Theory introduction

The next few posts will be following me on my journey through the book Category Theory, by Steve Awodey. I’m using the second edition, if anyone wants to joi...

Motivational learning

In which I am a wizard.

2014

Latin translation tips

I’m clearing out my computer, and found a file which may as well be here.

Matrix puzzle

I recently saw a problem from an Indian maths olympiad:

Film recommendation, Interstellar

I’ve just come back from seeing Interstellar, a film of peril and physics. This post will be spoiler-free except for sections which are in rot13.

Christmas carols

In which I provide my favourite carols and my favourite renditions of them.

Sum-of-two-squares theorem

Wherein I detail the most beautiful proof of a theorem I’ve ever seen, in a bite-size form suitable for an Anki deck. I attach the Anki deck, which contains ...

Python, script shadowing

A very brief post about the solution to a problem I came across in Python.

Parables, chapter 1, verses 1-10

One day, a group of investors came to Bezos in the Temple and begged of him, “You are known throughout the land for your wisdom. Please tell us: what lessons...

Perfect pitch

I have a limited form of perfect (absolute) pitch, which I am sometimes asked about. Often it’s the same questions, so here they are. No doubt people with be...

Music practice

A couple of weeks ago, someone opined to me that there was a type of person who was just able to sit down and play at the piano, without sheet music.

What maths does to the brain

In my activities on The Student Room, a student forum, someone (let’s call em Entity, because I like that word) recently asked me about the following questio...

Solvability of nonograms

Recently, a friend re-introduced me to the joys of the nonogram (variously known as “hanjie” or “griddler”). I was first shown these about ten years ago, I t...

Possible cons of Soylent

I have seen many glowing reviews of Soylent, and many vitriolic naturalistic arguments against it. What I have not really seen is a proper collection of cred...

Proof that symmetric matrices are diagonalisable

This comes up quite frequently, but I’ve been stuck for an easy memory-friendly way to do this. I trawled through the 1A Vectors and Matrices course notes, a...

Discovering a proof of Sylvester's Law of Inertia

This is part of what has become a series on discovering some fairly basic mathematical results, and/or discovering their proofs. It’s mostly intended so that...

Sequentially compact iff compact

Prof Körner told us during the IB Metric and Topological Spaces course that the real meat of the course (indeed, its hardest theorem) was “a metric space is ...

Cayley-Hamilton theorem

This is to detail a much easier proof (at least, I find it so) of Cayley-Hamilton than the ones which appear on the Wikipedia page. It only applies in the ca...

Sample topology question

As part of the recent series on how I approach maths problems, I give another one here (question 14 on the Maths Tripos IB 2007 paper 4). The question is:

Useful conformal mappings

This post is to be a list of conformal mappings, so that I can get better at answering questions like “Find a conformal mapping from <this domain> to &...

Discovering a proof of Heine-Borel

I’m running through my Analysis proofs, trying to work out which ones are genuinely hard and which follow straightforwardly from my general knowledge base. I...

How to discover the Contraction Mapping Theorem

A little while ago I set myself the exercise of stating and proving the Contraction Mapping Theorem. It turned out that I mis-stated it in three different as...

A roundup of some board games

It has been commented to me that it’s quite hard to find out (on the Internet) what different games involve. For instance, Agricola is a game about farming (...

Rage, rage against the poet’s hardest sell

I feel that I can write a sonnet well. While sonnets are an easy thing to spout, It’s really hard to write a villanelle.

Writing essays

The aim of this post is twofold: to find out whether a certain mental habit of mine is common, and to draw parallels between that habit and the writing of es...

Introduction to functional programming syntax of Mathematica

Recently, I was browsing the Wolfram Community forum, and I came across the following question:

Denouement of Myst III: Exile

A long time ago, in a galaxy far far away, I completed Myst III: Exile. It’s a stupendously good puzzle game. For some reason, it popped into my mind again a...

The Creation

Once upon a time, before this bountiful age of Matter and Light, there was only the Fell. A single being, surrounded by Chaos, content to remain alone foreve...