Artificial intelligence is reshaping mathematical research. Recent advances in AI for mathematics have drawn widespread attention from researchers and the public, prompting the renowned mathematician and Fields medalist Terence Tao to call for a “rapid rethink” of the entire research field .
However, instead of simply letting AI models solve longstanding problems and prove conjectures that have challenged them for decades, mathematicians may also find ways to use these advances as new research tools.
By securing a Project Numina Fellowship , Institute of Science and Technology Austria (ISTA) Professor Tamás Hausel will develop “Project Sandbox”—a controlled digital research environment where human mathematicians and AI agents build, compute, prove, and collaborate at the frontier of mathematical knowledge in a domain not yet formalized by any proof assistant.
Using a family of open conjectures as an input, Project Sandbox will develop a new theory to prove them—with every step machine-checked under the direction of a human mathematician. According to Hausel, the Numina-Lean-Agent , an interactive mathematical proof assistant introduced earlier this year, served as the inspiration and practical starting point for the architecture of Project Sandbox.
Meanwhile, the team has already developed an interactive visualization tool, which they call the “ eyepiece ”, to visualize the sandbox in action.
“Eventually, we plan to adapt the eyepiece for virtual reality and add tools that allow users to interact directly with the sandbox’s computations,” Hausel says.
A ‘research institute’ for AI agents—in a sandbox
With specialized agent roles and a defined workflow, Project Sandbox will operate similarly to a digital ‘research institute’ for AI agents—under the direction of a human mathematician.
“The sandbox will work as though it were a research institute dedicated to a single area of research,” Hausel explains. “A human mathematician sets the research agenda and evaluates which results are important, while the AI agents develop the necessary tools, formulate conjectures, attempt proofs, and review one another’s work.”
Importantly, Project Sandbox is designed so that nothing enters the record until a so-called computer algebra oracle has vetted the statement and a “proof kernel” has certified the proof.
In this context, an oracle is a formal tool that can provide answers to a specified class of questions in a single step. It verifies specific computational claims required by the system—much like performing a ‘background check.’
On the other hand, a proof kernel is a relatively simple independent computer program akin to a “proof checker” that works like an autograder for a mathematics exam . It does not assess the elegance of an argument nor does it discover proofs or assess their significance; it simply verifies that formal proof is valid within a specified system.
An AI-assisted bridge between two mathematical fields
With Project Sandbox, Hausel and his group aim to develop a practical connection between two areas of mathematics called “representation theory” and “equivariant topology”.
“The project will test whether AI can help build a proof-producing bridge between these two rich mathematical worlds,” he explains. “Connecting concepts such as quantum groups and Langlands classification in representation theory with affine Schubert varieties and GKM graphs in equivariant topology will ultimately help us build an AI-assisted framework for transferring ideas between algebra and geometry.”
When Hausel presented his project to Numina in June, he thought that the image of a ‘mathematical universe in a sandbox’ on his title slide seemed somewhat like science fiction.
“Amazingly, after only three weeks of work, the sandbox began running on my office computer as shown on the illustration,” he says. “We have already proved an important result, and we are well on our way to understanding this particular research area.”
Numina: A Paris-based international initiative
Project Numina is a global nonprofit headquartered in Paris, France. As an open-science collaboration, its mission includes developing AI for formal reasoning and fostering human-AI collaboration in mathematics. Numina brings together Olympiad medalists, young mathematicians, and machine-learning engineers to build open-source AI and explore new frontiers in mathematics.
The Project Numina Fellowship is designed for research groups worldwide interested in accelerating their research with AI tools designed for mathematical reasoning. The fellowship supports teams in co-developing solutions to deep and ambitious research problems at the forefront of scientific and mathematical research.
The Numina team is guided by the belief that “mathematics transcends intelligence like an endless ocean only the mind can sail.” With this new fellowship, Hausel and his group at ISTA will now build an AI-assisted system that will help them explore new, uncharted mathematical territory.