Xena
Mathematicians learning Lean by doing.
- By Kevin Buzzard
- Based in United Kingdom
- Roughly three posts per year
- First post on
Posts per year
| Year starting | Posts |
|---|---|
| 2021 | 5 |
| 2022 | 4 |
| 2023 | 2 |
| 2024 | 3 |
| 2025 | 0 |
Any gaps could be due to errors when fetching the blog’s feed.
Most recent posts
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. What is o3? What is FrontierMath? A language model, as probably …
So I’m two months into trying to teach a proof of Fermat’s Last Theorem (FLT) to a computer. Most of “how it’s going” is quite tedious and technical to explain: to cut a long story …
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 …