@davidbessis.bsky.social The curious case of broken theorems (Mathematics shouldn't survive logical errors—yet it does). ~ David Bessis. davidbessis.substack.com/p/the-curiou... #Math #ITP #LeanProver

🎉 Lean 4.22.0 is here! It represents the culmination of our Year 2 roadmap! Including:

🧠 New grind tactic (SMT-style automated reasoning)

🏗️ New compiler (major performance foundation)

Read the release notes: lean-lang.org/doc/reference/latest/releases/v4.22.0/

#LeanLang #LeanProver

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

Thoughts on AI and the IMO.

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

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

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

[RDV 16h !] Un projet collaboratif a formalisé la preuve du théorème de Fermat pour l’apprendre à un ordinateur. Quel est l’enjeu de cette formalisation ? Qu’est-ce qu’un assistant de preuve et quel est son rôle en mathématiques ? tinyurl.com/2dfebe9j avec Riccardo Brasca et Assia Mahboubi

Lean Together 2025 is happening (online conference: details leanprover-community.github.io/lt2025/). I've put the videos for day 1 of the conference up on YouTube: www.youtube.com/watch?v=ZPPD...

The fishbone conjecture (the Aharoni–Korman conjecture) is a 30-year-old natural conjecture on the structure of partially-ordered sets. It was *dis*proved (!) in November by Lawrence Hollom . Bhavik Mehta has now formalized the counterexmple in Lean github.com/b-mehta/Ahar... .

Litt was lucky -- he could give counterexamples to results claimed in the literature. Those working in the Langlands philosophy are less lucky, because our understanding of what should be true is far beyond what we can prove. I'm formalizing Fermats Last Thm to check that at least we got that right.