# Author Archives: xenaproject

## Does anyone “know” a proof of Fermat’s Last Theorem?

So there’s a piece in Vice which quotes me as saying that I fear “all published maths is wrong”. Of course this is nonsense: indeed, as every mathematician knows, some published maths is wrong, but the vast majority of it … Continue reading

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

## Proofs are not programs

A proof, in the sense understood by modern mathematicians, is not always a program. Continue reading

## The inverse of a bijection.

Constructing the inverse of a bijection in Lean can be tricky for beginners. Continue reading