Xena

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) … Continue reading →

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 →

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 →

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 →

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 →

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 →

My feed was recently clogged up with news articles reporting that Sam Altman thinks that AGI is here, or will be here next year, or whatever. I will refrain from giving even more air to this nonsense by linking to … Continue reading →

So the big news this week is that o3, OpenAI's new language model, got 25% on FrontierMath. Let's start by explaining what this means. Continue reading →

So I'm two months into trying to teach a proof of Fermat's Last Theorem to a computer. We already have one interesting story, which I felt was worth sharing. Continue reading →