Update on XTX Markets' AI for Maths Philanthropy

Given recent AI-powered developments in maths, and the wider acceleration of AI capabilities, XTX Markets is taking steps to update its philanthropy in this space.

These developments have been widely covered: from disproving the Unit-Distance Conjecture in May, to auto-formalising Fermat’s Last Theorem and solving the Navier-Stokes Problem in the past two weeks. In a recent press release, OpenAI claimed that its next generation models are even more capable than Astra, so there is reason to expect the trendline to continue.

AI tools offer us the potential to unlock a golden age of mathematical discovery. We could see decades of progress in the next year alone. This progress cannot be taken for granted, though, as the use of these tools is already disrupting the technical and community infrastructure that mathematicians have relied on to produce, share, interrogate, refine, and distil knowledge.

XTX Markets believes in an optimistic vision for the future of maths, centred around a thriving community of mathematicians, and combined with AI tools and robust norms to support high-quality mathematics. Our philanthropy will be directed towards this vision.

Over the last three years, XTX Markets and its founder, Alex Gerko, have committed >$50mn to open-source projects in the AI for maths space, including: $37mn to the AI for Math Fund, $10mn to Lean FRO, $6.5mn to Mathlib; and €3mn to Numina.

Going forward, we will continue to focus on breakthrough research, talent development and a healthy maths ecosystem, while also encouraging innovation and adjustment to new realities. In practice, this will mean discontinuing some grants, expanding others, and beginning to fund a range of new projects and experiments.

AIMO Prize

After careful consideration, including taking views from the AIMO Prize Advisory Committee, we have decided to close the AIMO Prize, including not progressing with the Grand Prize. We will collate all open-source artefacts in due course, and reallocate the unspent funds to other AI for maths initiatives, starting immediately.

The first AIMO progress prizes, held in 2024 and 2025, led to high-quality solutions by Numina and NemoSkills, and both ran out clear winners. In this year’s AIMO progress prize, however, most teams used the same base model, gpt-oss-120b, and built upon the same notebook, which led to a strong clustering of scores. The contest did produce valuable outputs, but these were driven more by the organiser-led review-rebuttal process and the extra prizes, such as the Corpus Prize and the Write-Up Prize, rather than top-scoring teams on the leaderboard.

Today, as well as the rapidly improving capabilities of frontier models, open-weight models are also claiming to achieve perfect scores on International Mathematical Olympiad problem sets, and so the AI for maths frontier has now shifted definitively to research mathematics.

Therefore, while the eligibility, parameters and rules for the Grand Prize had yet to be finalised, the contest, as originally conceived, is now unlikely to meaningfully incentivise valuable work. Our options were either to run an open-weight version that would essentially be a lottery, or to run a highly-restrictive version, allowing only fully open-source models and punitive compute limits. In our view, neither option would satisfy the intended spirit of the prize: to spur the open development of AI models that can reason mathematically.

We believe that the AIMO Prize has been a success. It has had widespread engagement: e.g. AIMO Progress Prize 3 is the largest reasoning competition ever held on Kaggle, and all three AIMO progress prizes are in the top 20 for prize money awarded. And it has supported various contributions to the field: e.g. Numina has continued to release several open-source outputs, most recently a formalisation of the Kakeya Conjecture. In total, >8,000 participants entered AIMO competitions and >$1.6mn was awarded. (See Appendix for further detail.)

We are grateful to everyone who has supported the AIMO Prize, including: Simon Frieder, who led the project; the AIMO Advisory Committee, who were generous with their time and wisdom; the problem composers, who worked behind the scenes to ensure that test data did not leak; Kaggle, which ran the competitions brilliantly, and did so on a fully pro bono basis; and – most importantly – the participants, whose contributions helped to advance the field.

Going Forward

Our priority now is to partner with the mathematics community to develop an optimistic vision for the future. As part of this, we believe that realistic solutions must include compute-intensive frontier models, as well as other AI tools, including some that can be run locally. But to unlock this golden age of mathematical discovery, we need more than AI tools; we need the technical and community infrastructure that allows us to produce high-quality mathematics. To this end, we are delighted to announce the first in a series of new grants.

Technical infrastructure

$10mn to Lean FRO. Lean is a focused research organisation, run by Convergent Research. Lean provided the verification layer in the auto-formalisation of Fermat’s Last Theorem, the solution to Navier-Stokes and many other high-profile AI for maths results. Formalisation with Lean makes a critical contribution to ensuring trusted output within the AI for maths ecosystem. The grant will cover Lean FRO’s core operating costs to 2030, providing a secure platform to continue and expand its crucial work.

$10mn to the Mathlib Initiative. Mathlib provided the formal foundation for various landmark results, including the auto-formalisation of Fermat's Last Theorem, and the verification of many highly complex proofs, such as the main theorem of liquid vector spaces. The grant will cover the Mathlib Initiative’s core operating costs to 2030, enabling it to build out the library of formal mathematics – a "human genome project for maths" – from the basics to frontier research.

The Foundation for Science and AI Research. SAIR was co-founded by the Fields Medallist, Terence Tao, and the Nobel Laureate, Barry Barish, with the mission to guide AI with scientific principles for humanity. This grant will fund three state-of-the-art AI for maths competitions: the Andrews-Curtis Conjecture Challenge (Stage 1); the Lean Kernel Challenge (Stage 1); and the Inverse Galois Problem Challenge (Stage 2). All of SAIR’s competitions are run openly, with public datasets, reproducible evaluation and results that reflect the collective contributions of the mathematics community.

Community infrastructure

This summer, XTX Markets convened a group of 40 leading maths educators and researchers at Brocket Hall, UK, to start drafting a blueprint for developing the mathematicians of the future. The event was an exercise in collaborative problem-solving, with participants generating and mapping the goals, problems and solutions. We are now in discussions with participants about publishing the blueprint, and holding a wider series of events with the mathematics community to develop it further. We intend to make on-going investments in new projects and experiments that arise from this process.

Appendix – AIMO Prize Series

Competition summary statistics

	AIMO 1	AIMO 2	AIMO 3	AIMO Proof Pilot
Competition	Progress Prize 1	Progress Prize 2	Progress Prize 3	Proof Pilot
Featured code	Featured code	Featured code	Invite only
Dates	April 2024 to June 2024	October 2024 to April 2025	November 2025 to April 2026	June 2026
Teams	1,161	2,212	3,450	6
Participants	1,401	2,672	4,065	7
Submissions	60,200	83,294	131,034	48
Problem Difficulty	Up to AIME	Up to national olympiad	Up to IMO easy	Up to IMO medium
Solution Format	Numerical (0-999)	Numerical (0-999)	Numerical (0-99,999)	Written, proof-based
Winning Team	Numina	NemoSkills	Exalted Joseph	Yi-Chia Chen
Winning Score	29/50	34/50	44/50	29/42
Prize Pool (Advertised)	$1,048,576	$2,117,152	$2,207,152	$210,000
Prize Pool (Awarded)	~$263,952	~$527,904	~$617,904	$210,000

Totals across the AIMO Prize series: 6,829 teams; 8,145 participants; 274,576 submissions; $5,582,880 advertised; ~$1,619,760 awarded.

Nb – As with many other Kaggle competitions, the highest potential prize awards are restricted for exceptional performance. In the case of the AIMO progress prizes, the threshold was 47/50 on the final leaderboard. Prize awards were fixed for the AIMO Proof Pilot.

Comparison to other Kaggle competitions

Competition	Prize Pool (Advertised)	Prize Pool (Awarded)	Rank (Advertised)	Rank (Awarded)
AIMO 3	$2,207,152	$617,904	#1	#9
AIMO 2	$2,117,152	$527,904	#2	#10
AIMO 1	$1,048,576	$263,952	#8	#16

Notable outputs and achievements

A fully open-source LLM (including training data and checkpoints) that rivals Opus 4.8 (high effort) on IMO-level maths problems, created by the AIMO Proof Pilot winner Yi-Chia Chen: https://www.kaggle.com/competitions/ai-mathematical-olympiad-proof-pilot/discussion/715176
Highly cited winners and artefacts: write-ups by AIMO progress prize-winning teams have been cited >400 times, including NemoSkills’ write-up, which has been cited >150 times: https://arxiv.org/abs/2504.16891
An engine for science: AIMO Progress Prize 3 resulted in 60 released papers and datasets, totalling ~1m datapoints: https://www.kaggle.com/competitions/ai-mathematical-olympiad-progress-prize-3/discussion/708484
Negative results published: several write-ups from AIMO Progress Prize 3 covered how to train the gpt-oss-120b model and reported negative results, helping others to avoid known problems: https://www.kaggle.com/competitions/ai-mathematical-olympiad-progress-prize-3/writeups/a-practitioners-plateau-on-gpt-oss-120b-mxfp4
A collaboration with OpenAI in March 2025, which tested private Open AI models against top AIMO Prize teams and, at the time, was the most rigorous evaluation of olympiad-level maths problems: https://aimoprize.com/updates/2025-09-05-the-gap-is-shrinking
A high-quality dataset of >400 original, unreleased olympiad-level problem-solution pairs, of which >200 underwent extensive manual review by experts and were used in the AIMO Prize competitions, and which may be used as uncontaminated benchmarks in the future.
A large and highly-engaged Kaggle community: the AIMO progress prizes attracted interest from Kaggle Grandmasters, and engineers at top companies such as Nvidia, Microsoft and SakanaAI. Write-ups from many of these participants created valuable resources for the AI for maths community.