### Patrick Stevens

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

# All Posts

## In favour of recursive functions, not imperative constructs, to make loops

Cross-posted at the G-Research official blog

## Defunctionalisation

Defunctionalisation: an underappreciated tool for writing good software

## Dependent types overview

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

## 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...

## 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

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...

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.

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.

## 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 ...

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...

## Smartphone Charter

I am shortly to receive a new Nexus 5. I am determined not to become a smartphone zombie, and so I hereby commit to the following Charter.

## Three explanations of the Monty Hall Problem

Earlier today, I had a rather depressing conversation with several people, in which it was revealed to me that many people will attempt to argue against the ...

## The Training Game

The book Don’t Shoot the Dog, by Karen Pryor, contains a simple exercise in demonstrating clicker training. This is a very successful technique used to produ...

## The Jean-Paul Sartre Cookbook

Many thanks to the Guru Bursill-Hall for bringing this tract to my attention through his weekly History of Maths bulletins. It was originally written in 1...

## Markov Chain card trick

In my latest lecture on Markov Chains in Part IB of the Mathematical Tripos, our lecturer showed us a very nice little application of the theorem that “if a ...

## My quest for a new phone

*This post is unfinished, and may never be finished - I have decided that the Nexus 5 is sufficiently cheap, nice-looking and future-proof to outweigh the bo...

## How to do Analysis questions

This post is for posterity, made shortly after Dr Paul Russell lectured Analysis II in Part IB of the Maths Tripos at Cambridge. In particular, he demonstrat...

## The Ravenous

Once upon a midnight dreary, while I pondered, weak and weary, I required a snack to feed me. Reaching in the kitchen drawer - With the scissors, cut the wra...

## Training away mental bias

In which I recount an experiment I have been performing. Please be aware that in this article I am in “meaning what I say” mode.

## Meaning what you say

In conversation with (say, for the purposes of propagating a sterotype) humanities students, I am often struck by how imprecisely language is used, and how m...

## Plot Armour

Wherein I dabble in parodic fiction. The title refers to the TV Tropes page on Plot Armour, but don’t follow that link unless you first resolve not to click ...

## How to prove that you are a god

I came across an interesting question while reading the blog of Scott Aaronson today. The question was as follows:

## Stumbled across 14th September 2013

On the merits of silence (I wholeheartedly agree): http://www.nytimes.com/2013/08/25/opinion/sunday/im-thinking-please-be-quiet.html

## Slightly silly Sylow pseudo-sonnets

This is a collection of poems which together prove the Sylow theorems.

I’ve been learning some basic topology over the last couple of months, and it strikes me that there are some very confusing names for things. Here I present ...

## Stumbled across 24th August 2013

The much-vaunted Hyperloop looks really cool, if it could ever be built: http://arstechnica.com/business/2013/08/hyperloop-a-theoretical-760-mph-transit-s...

## How to punt in Cambridge

When in Cambridge…

## My experiences with flow

I’m in the middle of reading Flow, by Mihály Csíkszentmihályi, and so far, I love it. It describes the “flow state” of consciousness, that state of “everythi...

## Thinking styles

All the way back into primary school (ages 4 to 11 years old, in case a non-Brit is reading this), we have been told repeatedly that “people learn things in ...

## Stumbled across 11th August 2013

A thousand times this: http://www.webcitation.org/6IdkckgOX A possible fix for the “economic problem of democracy”: http://hanson.gmu.edu/futarchy.html ...

## Stumbled across 4th August 2013

An ad developer has misgivings: http://seriouspony.com/blog/2013/7/24/your-app-makes-me-fat Hint for dealing with some automated phone helplines - swear...

## New computer setup

In case I ever have to get a new computer (or, indeed, in case anyone else is interested), I hereby present the (updating) list of applications and so forth ...

## On to-do lists as direction in life

Getting Things Done has gathered something of a cult following [archived due to link rot] since its inception. As a way of getting things done, it’s pretty g...

## Stumbled across 29th July 2013

Hehe: http://www.pixartheory.com/ Wow - light trapped for a full minute: http://www.newscientist.com/article/dn23925-light-completely-stopped-for-a-reco...

## Metathought

I have recently discovered the game of Agricola, a board game involving using resources (family members, stone, etc) to build a thriving farm. The game is tu...

## Stumbled across 24th July 2013

This is something I will try at some point, probably when I get back to uni: http://www.bulletproofexec.com/how-to-make-your-coffee-bulletproof-and-your-m...

## The Orbit/Stabiliser Theorem

The Orbit/Stabiliser Theorem is a simple theorem in group theory. Thanks to Tim Gowers for the proof I outline here - I find it much more intuitive than the ...

## On Shakespeare

I’ve now seen two Shakespeare plays at the Globe - once in person, to see A Midsummer Night’s Dream, and once with a one-year-and-eighty-mile gap between vie...

## My objection to the One Logical Leap view

A large chunk of the reason why changing someone’s mind is so difficult is the fact that our deeply-held beliefs seem so obviously true to us, and we find it...

## The Multiple Drafts view of consciousness

I’ve been reading one of Daniel Dennett’s books, Consciousness Explained. Aside from the fact that the author has an incredible beard and is therefore correc...

## Prerequisites for hypothetical situations

Usually when I discover (or, more rarely, think up) a thought experiment about a moral point, and discuss it with an arbitrary person whom I will (for conven...

## Stumbled across 13th July 2013

This is really quite heartwarming: http://www.reddit.com/r/Random_Acts_Of_Pizza/ Interesting article on current trends in fiction: http://www.locusmag.c...

## A framework for discussing "pricelessness"

Sometimes some people argue that certain things are “priceless” - that is, worth an infinite amount of money to them. I posit that what this really means is ...

There was once a small website devoted to noting the more interesting quotes from our more idiosyncratic lecturers. It has sadly vanished from the web - alth...

## Stumbled across 9th July 2013

Being bored over the summer holiday, I decided that I would document the cool things I ran across on the Internet. Over the last week, there have been many o...

## An obvious improvement to tennis

So yesterday the Wimbledon tennis tournament was decided. The system for verifying whether the tennis ball is out or not (and hence whether play for the poin...

## Mundane magics

I have stumbled across a LessWrong post on the importance of seeing what is real for just how cool it is. It lists such examples as:

## Cambridge vocab - a guide for the mystified

There is an awfully large collection of confusing words you will encounter on first coming to study at Cambridge. You pick them up really quickly in the natu...

I wrote this when I was excessively bored during exam term of my first year. It may grow as I get better at working (I’m something of a revisionist). The adv...

## In which I augment the lexicon

(This is my first post written in Dvorak; accordingly, it is a bit shorter than I would like, since I am very slow at it. Tsuyoku naritai, and all that.)

## Sylow theorems

(This post is mostly to set up a kind of structure for the website; in particular, to be the first in a series of posts summarising some mathematical results...

Hello all!

## CUCaTS Puzzlehunt

At the end of last (that is, Lent 2012-2013) term at Cambridge, I took part in the Cambridge University Computing and Technology Society Puzzlehunt (for some...