Christmas dinner notes

My notes on the production of a Christmas dinner.

Anki as Learning Superpower

Some techniques to help you get more out of Anki.

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

How to write loops immutably and safely.


An underappreciated tool for writing good software.

Dependent types overview

A quick overview of dependent types.

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 pointed out in the paper) it “builds itself”.

A Free Market

The story of Martin’s search for a kaki fruit.

Be a Beginner

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 Thomas Forster (to whom I owe many thanks for exposing me to such an interesting subject, and for agreeing to supervise the essay).

The use of jargon

Why jargon is a really useful thing to have and use.

Finitistic reducibility

A quick overview of the definition of the mathematical concept of finitistic reducibility.

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 fairly crucial last step, on account of the notes not yet being complete.

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 in one. (In fact, that blurb now contains an overview of how we may use modular machines to produce a group with insoluble word problem, and how to use them to embed a recursively presented group into a finitely presented one.) A modular machine is like a slightly more complicated version of a Turing machine, but it has the advantage that it is easier to embed a modular machine into a group than it is to embed a Turing machine directly into a group.

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.

Another Monty Hall explanation

Recall the Monty Hall problem: the host, Monty Hall, shows you three doors, named A, B and C. You are assured that behind one of the doors is a car, and behind the two others there is a goat each. You want the car. You pick a door, and Monty Hall opens one of the two doors you didn’t pick that he knows contains a goat. He offers you the chance to switch guesses from the door you first picked to the one remaining door.

Clojure and Exercism

I’ve been trying to learn Clojure through Exercism, a programming exercises tool. It took me an hour to get Hello, World! up and running, so I thought I’d document how it’s done. I’m using Leiningen on Mac OS 10.11.4.

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 finite injury priority method, and the proof is cribbed entirely from Dr Thomas Forster.

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 being interested in representable functors: they are basically “those with left adjoints”, up to minor quibbles.

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. I should note that this document contains no motivation of any kind. It is simply an exercise in symbol-shunting, and it has no clever ideas in it.

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 versions. Comments and corrections would be very much appreciated, because there is an awful lot of work involved in proving those theorems. It would be good to know of any parts where the argument is unclear, unmotivated, too long-winded, or wrong.