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 exciting developments centering on Erdős problems, especially involving the formalization of old and n…

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

Yes exactly! It's easy to get the "divides" ordering confused with the "less or equal to" ordering becase a | b usually implies a <= b. But everything divides zero, whereas everything is less than infinity.

If we said that infinite groups had "order 0" (i.e. "order" meant "size if it's finite, and 0 if not"), and elements of infinite order also had order 0, then the standard theorems about order of the element/subgroup dividing the order of the group would be true even in the infinite case.

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...

Public view of Lean | Zulip team chat Browse the publicly accessible channels in Lean without logging in.

Apparently so:
leanprover.zulipchat.com#narrow/chann...

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 ℝ?

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 in the last few days, which have inspired me to write about the question more broadly. Fir…

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.

AI at IMO 2025: a round-up 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 …

xenaproject.wordpress.com/2025/08/03/a... is a summary of what happened in 2025.

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/

Public view of Lean | Zulip team chat Browse the publicly accessible channels in Lean without logging in.

Good question. They're available on my hard drive but Simons never asked for them. I've uploaded them to the Lean Zulip here leanprover.zulipchat.com#narrow/chann...

YouTube video by Simons Foundation Kevin Buzzard - Where is Mathematics Going? (September 24, 2025)

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??

Of course Barbara! Thanks for asking!

Amongst the projects funded is my project www.renaissancephilanthropy.org/a-dataset-of... to create what in 2025 is a super-hard dataset of pairs (informal hard proof, formal statement) of recent results from top journals. The challenge for machine is to formalise the rest of the paper.

AI for Math Winners Page — Renaissance Philanthropy – A brighter future for all through science, technology, and innovation

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.

Mathematical Research Engineer — Renaissance Philanthropy – A brighter future for all through science, technology, and innovation

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.

Mathematics is also incomplete (assuming it's consistent) and that hasn't stopped lean from engaging with it at research level

AI Crushed the Math Olympiad—Or Did It? AI models supposedly did well on International Math Olympiad problems, but how they got their answers reminds us why we still need people doing math

@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...

Could you ever envisage lean being useful to verify nontrivial code written in common programming languages or is this asking too much?

I absolutely agree; IPAM is the notable absentee from the list. I organised a conference there in 2023 www.ipam.ucla.edu/programs/wor... bringing together people from mathematics and machine learning and formal methods, and it was a fascinating week!

NSF invests over $74 million in 6 mathematical sciences research institutes The U.S. National Science Foundation is investing over $74 million in six research institutes focused on the mathematical sciences and their broad applications in all fields of science, technology and...

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...

Lol that was me a few years ago

A level from the computer game "Baba is you"

Sunday afternoon.

AI at IMO 2025: a round-up 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 …

Thoughts on AI and the IMO.

xenaproject.wordpress.com/2025/08/03/a...

I did read parts of Langlands document about defining local epsilon factors locally and it was just page after page of representation theory (so it looked like groups acting on vector spaces)

I have never read the algebraic proof of the first inequality in global class field theory, I've just heard that it exists. I read the analytic proof last week though :-) The elementary proof of the prime number theorem still has plenty of basic real analysis in it.

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