xenaproject
- Boris Alexeev writes on how he's been experimenting with AI to solve Erdos Problems: xenaproject.wordpress.com/2025/12/05/f...
- 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...
- 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 ℝ?
- 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.
- 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.
- 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.
- 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 by xenaproject@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...
- 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...
- Sunday afternoon.
- Thoughts on AI and the IMO. xenaproject.wordpress.com/2025/08/03/a...
- 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.
- 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.
- 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...
- 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!
- 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".
- 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...
- @profkinyon.bsky.social you might like this one
