@xenaproject.bsky.social
Boris Alexeev writes on how he's been experimenting with AI to solve Erdos Problems: xenaproject.wordpress.com/2025/12/05/f...
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…
xenaproject.wordpress.com
December 5, 2025 at 3:10 PM
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.
November 15, 2025 at 2:29 PM
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.
November 15, 2025 at 10:17 AM
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
November 15, 2025 at 10:15 AM
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
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...
Apparently so:
leanprover.zulipchat.com#narrow/chann...
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
October 28, 2025 at 11:53 AM
Apparently so:
leanprover.zulipchat.com#narrow/chann...
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?
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.
xenaproject.wordpress.com/2025/08/03/a... is a summary of what happened in 2025.
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
October 22, 2025 at 10:49 AM
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/
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/
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...
Public view of Lean | Zulip team chat
Browse the publicly accessible channels in Lean without logging in.
leanprover.zulipchat.com
October 4, 2025 at 2:19 PM
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...
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??
Of course Barbara! Thanks for asking!
September 18, 2025 at 3:08 PM
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.
www.renaissancephilanthropy.org
September 18, 2025 at 8:25 AM
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.
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.
Mathematics is also incomplete (assuming it's consistent) and that hasn't stopped lean from engaging with it at research level
August 12, 2025 at 2:04 PM
Mathematics is also incomplete (assuming it's consistent) and that hasn't stopped lean from engaging with it at research level
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...
Could you ever envisage lean being useful to verify nontrivial code written in common programming languages or is this asking too much?
August 6, 2025 at 10:31 PM
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!
August 4, 2025 at 3:34 PM
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 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...
Lol that was me a few years ago
August 3, 2025 at 11:03 PM
Lol that was me a few years ago