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

The construction of local epsilon factors in the Langlands program was done by Langlands in an unpublished document which is hundreds of pages long. Then Deligne discovered a global construction which uses L-functions at some point and which fits into 30 pages

The fact that there exists a class formation for global fields (this is a higher reciprocity statement in number theory) boils down to proving two inequalities and traditionally one of them was done analytically (using L-functions like PNT) but now purely algebraic proofs are known.

Thanks for asking Barbara. The salary range is £48,056 - £56,345 per annum. I made some enquiries and the visa question is infinitely more complicated because there are a gazillion different kinds of visas depending on the applicant. The price could range from hundreds to thousands.

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.

Description Please note that job descriptions are not exhaustive, and you may be asked to take on additional duties that align with the key responsibilities ment...

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.

Lean FRO and Mathlib receive $10M from XTX Markets Founder Alex Gerko to further advance the use of AI for mathematical research — Renaissance Philanthropy – A brighter future for all through science,... FOR IMMEDIATE RELEASE July 24, 2025 Contact: media@renphil.org ; richard.hillary@xtxmarkets.com ; pr@convergentresearch.org

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

Note that no official IMO markers were involved in the marking of the solutions. I am also unclear about whether many solutions were generated and then humans chose the ones most likely to be correct, or whether the machine gave one "final answer" to each question with no human intervention.

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

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

Urysohn's lemma. Where do the numbers come from?

GitHub - teorth/analysis: A Lean companion to Analysis I A Lean companion to Analysis I. Contribute to teorth/analysis development by creating an account on GitHub.

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!

Mathematics and AI: Generating the Future How will AI change mathematics? - Turner Sims There’s no shortage of headlines proclaiming that AI will soon revolutionise everything — including mathematics — and leave no profession untouched. But what’s really happening behind the scenes? In t...

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

Big proof: formalizing mathematics at scale | Monday 09th June YouTube video by INI Seminar Room 1

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

They're worth a read! I was fortunate enough that their release was at a time when they were perfect material to read to my kids.

One of the questions is still open: whether there exists a finite magma with (some property) but not (some other peoperty); out of all the 44 million questions attacked by the project it is the only one which remains.

Yes, and this was one of the harder ones, so the question was which machines can solve it and how quickly and how efficiently.

@profkinyon.bsky.social you might like this one

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

See leanprover.zulipchat.com#narrow/chann... for the challenge. Can you find a proof which is easily human-comprehensible? Can you find a shorter proof than the 66-step proof which Tao links to? 2/2