Full Width [alt+shift+f] Shortcuts [alt+shift+k]
Sign Up [alt+shift+s] Log In [alt+shift+l]

Xena

Xena
What is a quotient? Undergraduate mathematicians usually have a hard time defining functions from quotients in Lean,...
4 weeks ago
17
4 weeks ago
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 →
Xena
Fermat’s Last Theorem — how it’s going So I'm two months into trying to teach a proof of Fermat's Last Theorem to a computer. We already...
2 months ago
9
2 months ago
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 →
Xena
Can AI do maths yet? Thoughts from a mathematician. So the big news this week is that o3, OpenAI's new language model, got 25% on FrontierMath. Let's...
2 months ago
9
2 months ago
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 →
Xena
Think of a number. My feed was recently clogged up with news articles reporting that Sam Altman thinks that AGI is...
a month ago
9
a month ago
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 →
Xena
Lean in 2024 A huge amount happened in the Lean theorem prover community in 2023; this blog post looks back at...
a year ago
8
a year ago
A huge amount happened in the Lean theorem prover community in 2023; this blog post looks back at some of these events, plus some of what we have to look forward to in 2024. Modern mathematics I personally am a … Continue reading →
Xena
2022 Xena Project undergraduate workshop I have funding to run an undergraduate workshop! When? 26th to 30th September 2022 (the week before...
over a year ago
7
over a year ago
I have funding to run an undergraduate workshop! When? 26th to 30th September 2022 (the week before term starts for many people in the UK). What? A week-long in person workshop including a bunch of working on group projects in … Continue reading →
Xena
Beyond the Liquid Tensor Experiment The liquid tensor experiment is now fully completed. Continue reading →
over a year ago
Xena
Formalising modern research mathematics in real time (This is a guest post by Bhavik Mehta) On March 16, 2023, a paper by Campos, Griffiths, Morris, and...
a year ago
5
a year ago
(This is a guest post by Bhavik Mehta) On March 16, 2023, a paper by Campos, Griffiths, Morris, and Sahasrabudhe appeared on the arXiv, announcing an exponential improvement to the upper bound on Ramsey numbers, an open problem since 1935. … Continue reading →
Xena
Lean 2022 round-up A brief survey post containing some of the things which happened in the Lean community in 2022. The...
over a year ago
5
over a year ago
A brief survey post containing some of the things which happened in the Lean community in 2022. The Liquid Tensor Experiment In December 2020, Fields Medallist Peter Scholze challenged the formal computer proof community to verify one of his theorems … Continue reading →
Xena
The Future of Interactive Theorem Proving? This is a guest post, written by Zhangir Azerbayev. Zhangir is an undergraduate at Yale, majoring in...
over a year ago
5
over a year ago
This is a guest post, written by Zhangir Azerbayev. Zhangir is an undergraduate at Yale, majoring in computer science and mathematics. He completed this work while visiting Carnegie Mellon’s Hoskinson Center for Formal Mathematics. Introduction The history of interactive theorem...
Xena
Teaching formalisation to mathematics undergraduates It’s been a hectic 2022 so far, but August is looking a lot calmer; this is the first of hopefully a...
over a year ago
4
over a year ago
It’s been a hectic 2022 so far, but August is looking a lot calmer; this is the first of hopefully a few blog posts this month catching up on various things. In this post I want to talk about the … Continue reading →