Boris Alexeev writes on how he's been experimenting with AI to solve Erdos Problems: xenaproject.wordpress.com/2025/12/05/f...

It's funny how mathematicians sometimes confuse 0 and infinity. We say that the characteristic of a field can be 0, but that the order of an element in a group can be infinity. These are two different conventions expressing the same idea. 1/2

ooh hello

Congratulations to Floris van Doorn and Christian Thiele for their new ERC grant for formalization of analysis in Lean www.mathematics.uni-bonn.de/en/news/will...

Here's the statement in Lean. How little can one get away with importing in order to prove this? Can it be proved by induction on max(l)-min(l) for example, avoiding the reals completely?

Fermat's Last Theorem is a famous example of a question which can be stated using only naturals and whose proof requires a lot of machinery. But in fact the AM-GM inequality, just for ℕ, can be stated purely using ℕ (clear denoms, raise everything to n'th power). Is there a simple proof avoiding ℝ?

xenaproject.wordpress.com/2025/10/22/f... A chat around what's been happening in the world of AI and Erdos problems, and what it highlights.

ItaLean : formal maths and AI in Italy (Bologna), Dec 2025. Lectures, hands-on tutorials, research talks from academia and industry etc. Register here pitmonticone.github.io/ItaLean2025/

My talk at the Simons Foundation last week is now up on YouTube youtube.com/watch?v=K5w7VS2sxD0 . It is a hopefully-comprehensible general audience talk about what I think is a big decision which mathematicians will have to decide whether to back or not.

My colleague Jon Mestel pointed out to me that whether you use the US 09272025 date system or the pretty-much-everywhere-else-in-the-world-and-far-saner 27092025 system, today's date is a perfect square, as is the current month and the year! Will this ever happen again??

Renaissance Philanthropy have announced the first 29 grants they've given from their AI For Math fund www.renaissancephilanthropy.org/ai-for-math-... . Interesting to see that around half of the funded proposals mention Lean.

The Mathlib Initative is hiring! www.renaissancephilanthropy.org/careers/math... (part-time contractor, helping to solve the "2000 PRs" issue, note the required qualifications) and www.renaissancephilanthropy.org/careers/devo... (full-time, solving distributed systems challenges). 14 Sept deadline.

@sciam.bsky.social gave me the opportunity to share some personal thoughts about the recently reported AI results from the #imo2025: www.scientificamerican.com/article/math...

NSF announces funding for ICARM: the Institute for Computer-Aided Reasoning in Mathematics, based in Carnegie-Mellon . Amazing! Carnegie-Mellon press release here: www.cmu.edu/news/stories... www.nsf.gov/news/nsf-inv...

Sunday afternoon.

Thoughts on AI and the IMO. xenaproject.wordpress.com/2025/08/03/a...

Featuring a sorry-free proof that 2+2=6

Why is this a worthwhile project? 1) It will create a hard dataset for autoformalization AI's; 2) It will force us to formalize the definitions of mathematical objects which are being used today in the top journals, thus making Lean's mathematics library more relevant to modern math researchers.

I am advertising for 4 post-docs to come to Imperial and formalize, in Lean, *statements* of theorems from recent issues of the top generalist pure mathematics journals. www.imperial.ac.uk/jobs/search-... Positions are for 2 years, start date 1st Oct this year. Deadline 15th August.

A new "Mathlib initiative" focussed around Lean's mathematics library has been announced. Thanks to the generosity of Alex Gerko and XTX Markets, there is finally an official entity focussed on growing this 21st century way of doing mathematics. www.renaissancephilanthropy.org/news-and-ins...

Floris van Doorn and his team at Bonn have finished formalizing both the classical theorem of Carleson (Fourier series converges almost everywhere) and a far-reaching generalisation (still unpublished) on doubling metric measure spaces. leanprover.zulipchat.com#narrow/chann...

Terry Tao has translated his "Analysis I" textbook into Lean! github.com/teorth/analy... Projects like this are tough to pull off, and need users to play through the levels and find and eliminate things which the formalization is making artificially hard. Fork the repo and give the exercises a try!

First volume of new diamond open access journal "Annals of Formalized Mathematics" just dropped: afm.episciences.org/volume/view/...

Markus Himmel has written a blog post about how to write a simple imperative program in Lean and then how to verify that the program is bug-free. markushimmel.de/blog/my-firs...

Some fundamental progress in formalized category theory in Lean including Freyd-Mitchell embedding.

Last chance to see @emilyriehl.bsky.social at the LMS next month!

I have a gig in Southampton next week! www.turnersims.co.uk/whats-on/mat... Thurs 19th June 2025, 4pm, tickets are free but need to be booked in advance, I'll be explaining what I learnt this week in Cambridge about where we are with AI and mathematics, and summarising for a general audience.

I'm at Big Proof this week. Bhavik Mehta's talk (video not yet up) contained a big surprise at the end: one of the references in a paper he's formalizing is an old 4-page paper about bounds for the ABC conjecture, and the paper has been completely *autoformalized* by Morph Labs' AI model "Trinity".

I'm teaching a computer a proof of Fermat's Last Theorem. Here's my talk from yesterday at the Newton Institute in Cambridge explaining how it's going. www.youtube.com/live/r-Vu_4s...

@profkinyon.bsky.social you might like this one

Let G be a magma (i.e a set equipped with a multiplication and no further axioms). Can you prove that if ∀ x y z, x = x(y((zx)y)) then ∀ x y z, x = x(y(z(xz)))? You can use a theorem prover, a language model, a SAT or SMT solver or even pencil and paper. Terry Tao is collecting proofs of this! 1/2

I think Courtney knows as well as I do what's going on here. A CS friend of mine told me that they'd set a homework problem about a family tree containing Homer, Marge, Bart, Lisa and Maggie, and some of the solutions she got had answers referring to other Simpsons characters not in the question.

Great Exhibition Road Festival 7th and 8th June, come play me at dots and boxes

Dang we should have youtube videos for every tactic www.youtube.com/watch?v=y6p0...

The US's National Science Foundation advisory committee for Mathematical and Physical Sciences has just been disestablished, by Presidential executive order. www.nsf.gov/executive-or...

The final proof in Tao's "Equational theories" Lean project has just been formalized! See Tao's blog post here github.com/teorth/equat... . All 22,028,942 theorems are now formally verified in Lean. A place to start reading about the project is here teorth.github.io/equational_t... .

Lean's maths library finally has the Lie algebra of a Lie group! github.com/leanprover-c... The library has been used to formalize research level mathematics but there are still a few things missing which I learnt as an undergrad, and this was one. Still no de Rham cohomology though...

They're doing affine group schemes along the way -- useful for FLT! Why doesn't Sophie Morel get a mention though? She's working on diagonalisable group schemes for the project.

Proving Fermat's Last Theorem in the Roundhouse Camden whilst listening to Jem Finer's Longplayer en.wikipedia.org/wiki/Longpla...

arxiv.org/abs/2503.21934 tl;dr: people think LLMs are getting good at maths because they're being tested on hard questions for which the answer is a number. But when you ask them for proofs (which is what mathematicians *actually* do) they score < 5% on average even at Olympiad (pre-uni) level.

I'll be speaking with Leo de Moura in Oxford on the afternoon of 6th May: we're giving the 2025 Strachey Lectures. Register here www.cs.ox.ac.uk/seminars/264...

I'll be challenging allcomers at dots and boxes at the Great Exhibition Road Festival on 7th/8th June: www.greatexhibitionroadfestival.co.uk/event/maths-...

Maxwell's equations in Lean: github.com/HEPLean/Phys... Part of a project by Joseph Tooby-Smith to formalize various parts of physics in Lean.

Applications are open for the 2025 Clay Math summer school in Oxford UK, on formalization of class field theory. If anyone knows of PhD students interested in one or more of class field theory, and formalization of mathematics, encourage them to apply! www.claymath.org/events/forma...

To my fellow screamers:

An update on a (basically failed) attempt of mine to make a database of hard number theory problems on the cheap.

Just merged and deployed the PR with an Italian translation of the Natural Number Game! Game currently available in English, Italian and Chinese; try it at adam.math.hhu.de#/g/leanprove... if you didn't already have a go. It's all about proving 2+2=4 (and some generalizations of this).

Interesting panel discussion on the new FrontierMath blog post epoch.ai/frontiermath... . Everyone seems to be in agreement that LLMs are going to get good at guessing numerical answers to hard maths qs. People at pains to point out that maths isn't about this. Best part was (1/2)

Quantum harmonic oscillator in Lean: heplean.com/CuratedNotes...

Terry Tao speaking on machine-assisted proofs: www.youtube.com/watch?v=5ZII... . This is quite a broad (and general audience) discussion on uses of language models, theorem provers and neural networks in mathematics.