Author Archives: xenaproject

About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College (and beyond) trained in the art of formalising mathematics on a computer.

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

Posted in Uncategorized | Tagged , , , | 9 Comments

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

Posted in General, number theory | Tagged , | 1 Comment

Lean does not (yet) have real manifolds.

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

Posted in General, Imperial, undergrad maths | Tagged , , , , , , , , , , , , , , , , | 7 Comments

A computer-generated proof that nobody understands

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

Posted in General | Tagged , , , , , , , , , , | Leave a comment

What is homotopy type theory? An amateur speaks.

Learning some Euclidean geometry helped me to understand the basics of what homotopy type theory is. Continue reading

Posted in undergrad maths | Tagged , , , , , , | 12 Comments

Proofs are not programs

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

Posted in computability | Tagged , , , | Leave a comment

The inverse of a bijection.

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

Posted in Learning Lean, M1F | Tagged , | 9 Comments