# Category Archives: General

## IMO 2019 Q1

Someone sent me a link to this year’s IMO questions this afternoon at work, and the first one caught my eye because it looked like a relatively straightforward functional equation question: find all such that . I’ve seen enough of … Continue reading

## Lean does not (yet) have real manifolds.

Lean does not yet have real manifolds, but there has been recent progress. Continue reading

## A computer-generated proof that nobody understands

Computers can find 1000 page proofs about simple things. Why not Shimura varieties? Continue reading

## What is the Xena Project?

Note (added June 2019); this (below) is an old blog post from 2018. You should really read the updated one here but I’ve left this original one just to preserve history. The current aims and ambitions of the Xena Project … Continue reading

## Formalising mathematics — a mathematician’s personal viewpoint.

Here is an overview of my current thoughts on formal proof verification systems in modern mathematics. 3d computer modelling software such as Blender can make virtual versions of abstract 3d mathematical figures such as truncated dodecahedra and so on. This … Continue reading

## Summer project

I am running a summer project with some students. I’ve sort-of lost count of how many; I think that around 25 people expressed an interest, but some didn’t start yet. In practice we seem to get around 10-15 people coming … Continue reading

## (a+b)^3

The problem This post is about the equation . This special case of the binomial theorem is the sort of thing that we would expect incoming students at my university to know, or at least to be able to compute … Continue reading