Funding will support Project Numina’s ambitious research roadmap to transform the landscape of mathematical reasoning formalization.

Project aims to accelerate the development of innovative and open-source AI tools for mathematicians and general progress in AI reasoning.

PARIS: Project Numina, a non-profit organization dedicated to advancing mathematical knowledge and accessibility through artificial intelligence, has received a €3 million grant from XTX Markets, the leading algorithmic trading firm. In accordance with Numina’s public benefit mission, all the results of the project will be released to the public.

As advancements in AI continue to transform the field of mathematics, access to state-of-the-art AI models for mathematical reasoning, along with their associated training datasets, remains limited. This lack of public availability significantly impedes both rigorous evaluation and widespread adoption by the scientific community. With the support of XTX Markets, Numina is embarking on a groundbreaking initiative to collect and publicly release a comprehensive database of up to one million formal mathematical problems and proofs. This effort will be complemented by the development and open-sourcing of advanced reasoning models, fostering greater collaboration and innovation in mathematical AI research.

Simon Coyle, Head of Philanthropy, XTX Markets said, “AI has huge potential to push the frontier of knowledge in mathematics. An important next step is developing open-source models for mathematical reasoning, so we are delighted to support Project Numina’s mission to create data and tools that will help accelerate progress towards this goal.”

Yann Fleureau, co-founder and President of Numina, said, “We are grateful to XTX Markets for their generous commitment to advance progress in mathematics. With their support, Numina will be able to publicly release datasets and AI models which will dramatically advance AI mathematical reasoning.”

Building the largest open dataset of mathematical reasoning in history

Last July, Numina publicly released NuminaMath, the largest database of mathematical problems and proofs in history (860,000 entries). Numina also built and released an AI model which won the AIMO progress prize #1, demonstrating national-level competitive math capabilities, winning $131,072.

Project Numina’s next objective is to build and release a corpus of up to 1 million formal exercises and proofs. The XTX Markets grant will support a major step on this journey by enabling the formalization of up to 100,000 items.

Mathematics to remain an open domain in the age of AI

Along with the development of the formal math dataset, Numina will pursue the development and open-source release of AI models specialized in mathematics.

“We are working on AI models to automatically prove theorems and formalize mathematical reasoning. We are very excited to see how our datasets and models will be used by the community,” said Jia Li, co-founder and Chief Scientist of Numina.

“Formalization tools such as Lean have the potential to bring huge benefits to mathematics, and are already starting to do so, but progress is held up by the significant investment of time it takes to learn and use these tools. If AI can be trained to perform formalization automatically to a high standard, this barrier will be removed, or at least dramatically reduced, and that is likely to be a game changer for how we produce and share mathematical content,” said Timothy Gowers, Fields Medalist and holder of the Combinatorics chair at the Collège de France and fellow of Trinity College Cambridge.

Numina plans a first public release of its research data and results by mid-2025 and is developing an interactive web interface to enable the general public to access its database for educational purposes.

About Numina

Numina is a non-profit organization and an open scientific collaboration fostering the development of human and artificial intelligence in the field of mathematics. In July 2024, Numina won the AIMO progress prize #1 and released publicly the largest dataset of mathematical problems and proofs.

Fonte: Business Wire