@xenaproject.bsky.social
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...
Will mathematical research results be verified by computers in the future?
www.mathematics.uni-bonn.de
November 6, 2025 at 4:38 PM
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?
October 26, 2025 at 11:05 AM
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 ℝ?
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 ℝ?
October 26, 2025 at 10:59 AM
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 ℝ?
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.
A chat around what's been happening in the world of AI and Erdos problems, and what it highlights.
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
October 22, 2025 at 2:43 PM
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.
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/
ItaLean 2025
pitmonticone.github.io
October 9, 2025 at 12:31 PM
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.
Kevin Buzzard - Where is Mathematics Going? (September 24, 2025)
YouTube video by Simons Foundation
youtube.com
October 3, 2025 at 4:50 PM
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??
September 27, 2025 at 3:58 PM
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.
AI for Math Winners Page — Renaissance Philanthropy – A brighter future for all through science, technology, and innovation
www.renaissancephilanthropy.org
September 18, 2025 at 8:21 AM
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.
Mathematical Research Engineer — Renaissance Philanthropy – A brighter future for all through science, technology, and innovation
www.renaissancephilanthropy.org
August 22, 2025 at 10:14 AM
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.
Reposted
@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...
www.scientificamerican.com/article/math...
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
www.scientificamerican.com
August 7, 2025 at 4:31 PM
@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...
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...
www.nsf.gov/news/nsf-inv...
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...
www.nsf.gov
August 4, 2025 at 3:22 PM
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...
www.nsf.gov/news/nsf-inv...
Sunday afternoon.
August 3, 2025 at 3:58 PM
Sunday afternoon.
Featuring a sorry-free proof that 2+2=6
⚛️📝 New on Overreacted: The Math Is Haunted
The Math Is Haunted — overreacted
A taste of Lean.
overreacted.io
July 31, 2025 at 7:54 AM
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.
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.
www.imperial.ac.uk/jobs/search-...
Positions are for 2 years, start date 1st Oct this year. Deadline 15th August.
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...
www.imperial.ac.uk
July 28, 2025 at 12:12 PM
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.
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.
www.imperial.ac.uk/jobs/search-...
Positions are for 2 years, start date 1st Oct this year. Deadline 15th August.
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...
www.imperial.ac.uk
July 28, 2025 at 12:10 PM
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.
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...
www.renaissancephilanthropy.org/news-and-ins...
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
www.renaissancephilanthropy.org
July 24, 2025 at 6:33 PM
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...
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...
Public view of Lean | Zulip team chat
Browse the publicly accessible channels in Lean without logging in.
leanprover.zulipchat.com
July 19, 2025 at 2:45 PM
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!
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!
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.
github.com
July 15, 2025 at 5:24 PM
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!
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/...
Annals of Formalized Mathematics - Volume 1
afm.episciences.org
July 15, 2025 at 5:14 PM
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...
markushimmel.de/blog/my-firs...
My first verified (imperative) program
One of the many exciting new features in the upcoming Lean 4.22 release is a preview of the new verification infrastructure for proving properties of imperative programs. In this post, I’ll take a fir...
markushimmel.de
July 6, 2025 at 4:03 PM
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...
markushimmel.de/blog/my-firs...
Some fundamental progress in formalized category theory in Lean including Freyd-Mitchell embedding.
Theorems about abelian categories (in Lean). ~ Markus Himmel, Joël Riou. leanprover-community.github.io/blog/posts/a... #ITP #LeanProver #Math
Theorems about abelian categories
Two significant results about abelian categories have recently been
added to mathlib. The first is that any Grothendieck
abelian category has enough injectives, and it follows from a
general construct
leanprover-community.github.io
June 20, 2025 at 5:26 PM
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!
🚨 Down to just 🔟 places left for this year's LMS General Meeting and Hardy Lecture, taking place at De Morgan House (and online) on 4 July and featuring speakers Emily Riehl and Clark Barwick @edinunimaths.bsky.social.
For further details and to register ➡️ www.lms.ac.uk/events/lms-g...
For further details and to register ➡️ www.lms.ac.uk/events/lms-g...
June 19, 2025 at 10:04 PM
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.
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.
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...
www.turnersims.co.uk
June 14, 2025 at 3:06 PM
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.
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".
June 12, 2025 at 3:36 PM
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".