Xena
FLT: Anthropic has beaten me to it
I guess technically it was revealed to the world by a coffee shop in Islington on Insta, but an hour...
a week ago
I guess technically it was revealed to the world by a coffee shop in Islington on Insta, but an hour later it was officially announced by Anthropic: one of their internal models, using the prove2.me platform, has formalized a complete … Continue reading →
Xena
The Annals Challenge
My team of post-docs funded by this Renaissance Philanthropy grant has constructed a dataset of 50...
13th Aug 2026
My team of post-docs funded by this Renaissance Philanthropy grant has constructed a dataset of 50 Lean statements, corresponding to 50 important recent mathematical theorems! The 50 theorems were all published in the Annals of Mathematics (a prestigious mathematical journal) …...
Xena
Human mathematicians are being outcounterexampled
It’s been an interesting few weeks for counterexamples. This post is basically my perspective of...
20th Jul 2026
It’s been an interesting few weeks for counterexamples. This post is basically my perspective of what has been going on in the world of formalization, AI tools and, in particular, counterexamples. Unit distance Two months ago today (20th May 2026), … Continue reading →
Xena
Formalizing Fermat workshop
I’m organizing a workshop in London on July 6th to 10th (2026) whose goal is to work on my...
15th May 2026
I’m organizing a workshop in London on July 6th to 10th (2026) whose goal is to work on my EPSRC-funded project formalizing Fermat’s Last theorem in Lean. The initial aim of the project was to reduce FLT to theorems known … Continue reading →
Xena
Accelerating mathematics
Let’s say that someone had a big pot of money, and wanted to use it to accelerate mathematical...
9th Feb 2026
Let’s say that someone had a big pot of money, and wanted to use it to accelerate mathematical discovery. How might they go about doing this? The traditional approach Historically it has been governments who have been driving this agenda, … Continue reading →
Xena
Formalization of Erdős problems
[This is a guest post by Boris Alexeev. Now over to Boris.] I’m here to tell you about various...
5th Dec 2025
[This is a guest post by Boris Alexeev. Now over to Boris.] I’m here to tell you about various exciting developments centering on Erdős problems, especially involving the formalization of old and new mathematics using artificial intelligence. Background As is … Continue reading →
Xena
Formal or not formal? That is the question in AI for theorem proving.
So it’s an interesting time for computers-doing-mathematics. A couple of interesting things happened...
22nd Oct 2025
So it’s an interesting time for computers-doing-mathematics. A couple of interesting things happened in the last few days, which have inspired me to write about the question more broadly. First there is the question on whether computers will ever prove … Continue reading →
Xena
AI at IMO 2025: a round-up
Setting the scene The 2025 International Mathematics Olympiad has come and gone. Reminder: this is...
3rd Aug 2025
Setting the scene The 2025 International Mathematics Olympiad has come and gone. Reminder: this is an exam for high-school kids across the world (each country typically sends six kids), comprising of two 4.5-hour exams each containing three questions, so six … Continue reading →
Xena
Think of a number: an update
A month or two ago I wrote this post which expressed my frustration with various issues around...
16th Mar 2025
A month or two ago I wrote this post which expressed my frustration with various issues around private datasets as a way of measuring the mathematical abilities of language models. More generally I was frustrated about the difficulty of being … Continue reading →
Xena
What is a quotient?
Undergraduate mathematicians usually have a hard time defining functions from quotients in Lean,...
9th Feb 2025
Undergraduate mathematicians usually have a hard time defining functions from quotients in Lean, because they have been taught a specific model for quotients in their classes, which is not the model that Lean uses. This post is an attempt to … Continue reading →
Full Width 
Shortcuts 
Sign Up 
Log In 
Articles 
Reading List 