Mathematician builds a digital sandbox where AI agents prove theorems under human command

Artificial intelligence has been moving through mathematics with a speed that few researchers anticipated, and the reaction from within the field has ranged from excitement to outright alarm. When recent AI systems began producing serious mathematical results, Fields medalist Terence Tao publicly called for a rapid rethink of how mathematical research should be organized. At the Institute of Science and Technology Austria (ISTA), professor Tamás Hausel has chosen a different response to that upheaval: rather than treating AI as an external force that might one day solve problems on its own, he is building a controlled environment in which human mathematicians and AI agents work side by side, with every claim machine-checked before it can enter the mathematical record. His vehicle for this experiment is a Project Numina Fellowship, awarded to support the development of what he calls Project Sandbox.

Project Sandbox is conceived as a self-contained digital research environment, a kind of sealed laboratory where AI agents can build, compute, prove, and collaborate at the frontier of mathematical knowledge. The domain Hausel has chosen is deliberately ambitious: an area of mathematics that has not yet been formalized by any proof assistant, meaning that no existing software infrastructure exists to verify work in that territory. The project takes as its input a family of open conjectures and aims to develop a new theory capable of proving them, with every step of the argument checked by machine under the direction of a human mathematician. The design is not speculative software vaporware. According to Hausel, the Numina-Lean-Agent, an interactive mathematical proof assistant introduced earlier this year, served as both the inspiration and the practical starting point for the architecture of the sandbox.

The way the sandbox is organized borrows more from the sociology of academic institutions than from conventional software design. Hausel describes it as a digital research institute for AI agents, complete with specialized roles and a defined workflow. A human mathematician, in this case Hausel and his group, sets the research agenda and evaluates which results are actually important, while the AI agents develop the necessary tools, formulate conjectures, attempt proofs, and review one another’s work. This division of labor is central to the project’s philosophy. The machine agents generate volume and speed, exploring many possible avenues of argument in parallel, while the human director supplies the judgment about which avenues matter and which results would constitute genuine mathematical progress rather than formally correct trivia.

What makes the architecture more than an elaborate chatbot pipeline is its verification layer. Project Sandbox is designed so that nothing enters the record until two independent checks have been passed. The first is a computer algebra oracle, a formal tool that can answer a specified class of questions in a single step. In this system, the oracle verifies specific computational claims required by the larger argument, functioning much like a background check on the numerical and algebraic assertions that a proof depends on. The second check is a proof kernel, a relatively simple and independent computer program that acts as a proof checker. Hausel compares it to an autograder for a mathematics exam: it does not assess the elegance of an argument, it does not discover proofs, and it does not judge their significance. It simply verifies that a formal proof is valid within a specified logical system. Together, these two mechanisms mean that the sandbox’s output is not a stream of plausible-sounding AI text but a chain of certified results.

This separation between generation and verification addresses one of the most persistent anxieties about AI in mathematics. Large language models can produce fluent mathematical prose, but fluency is not proof, and the history of the past few years is littered with plausible-looking arguments that collapse under scrutiny. By forcing every statement through an oracle and every proof through a kernel, the sandbox ensures that the AI agents cannot pollute the mathematical record with unverified material, no matter how confident their outputs appear. The human mathematician, meanwhile, retains control over the questions being asked and the interpretation of what has been established. The result is a system in which the weaknesses of machine reasoning are contained and its strengths, chiefly tireless exploration and rapid formal manipulation, are harnessed.

The scientific goal of the project is as concrete as its engineering is careful. Hausel and his group aim to build a practical connection between two areas of mathematics called representation theory and equivariant topology. Representation theory studies abstract algebraic structures by representing their elements as matrices and studying how those matrices act, and it underpins vast swaths of modern mathematics and physics, including the theory of quantum groups and the Langlands classification. Equivariant topology, by contrast, studies geometric spaces equipped with symmetries, and tools such as affine Schubert varieties and GKM graphs allow topologists to extract algebraic information from symmetric geometric objects. The project, in Hausel’s words, will test whether AI can help build a proof-producing bridge between these two rich mathematical worlds, connecting concepts such as quantum groups and Langlands classification on the algebraic side with affine Schubert varieties and GKM graphs on the topological side.

The significance of that bridge lies in what it would make possible. Mathematicians have long known that deep results in algebra and geometry often mirror one another, with the same underlying structures appearing in different guises across fields. When such connections are made rigorous, ideas can flow in both directions: a theorem proved in one language suddenly becomes a theorem in the other, and hard open problems in one field can be translated into more tractable forms in another. Building this transfer framework by hand is slow, painstaking work, because the dictionary between two fields must be constructed statement by statement and verified with total precision. An AI-assisted framework for transferring ideas between algebra and geometry, with machine-checked correctness at every step, could accelerate exactly this kind of dictionary building, which is one reason the fellowship’s reviewers found the proposal compelling.

The project has already moved from concept to working software with surprising speed. When Hausel presented his proposal to Numina in June, he admitted that the image of a mathematical universe in a sandbox on his title slide felt somewhat like science fiction. Yet after only three weeks of work, the sandbox was running on his office computer, producing the visualization that now illustrates the project. The team has also developed an interactive visualization tool, which they call the eyepiece, that allows researchers to watch the sandbox in action, observing how the agents compute and interact within their sealed environment. The longer-term plan is more ambitious still: Hausel says the team eventually intends to adapt the eyepiece for virtual reality and add tools that allow users to interact directly with the sandbox’s computations, turning an internal research instrument into something closer to an explorable mathematical world.

The fellowship behind the project comes from Project Numina, a global nonprofit headquartered in Paris, France, that operates as an open-science collaboration. Its mission is twofold: to develop AI for formal reasoning and to foster human-AI collaboration in mathematics. The organization brings together Olympiad medalists, young mathematicians, and machine-learning engineers to build open-source AI tools and explore new frontiers in mathematical research. Its fellowship program is designed for research groups worldwide that want to accelerate their work with AI tools built for mathematical reasoning, supporting teams in co-developing solutions to deep and ambitious problems at the forefront of science and mathematics. The Numina team summarizes its guiding conviction in a poetic register, holding that mathematics transcends intelligence like an endless ocean only the mind can sail, a sentiment that frames AI not as a replacement for mathematical thought but as a vessel for extending it.

For the community watching AI’s advance into mathematics, the ISTA project offers a template that is neither pure resistance nor pure surrender. Rather than waiting to see whether autonomous AI systems will eventually prove conjectures on their own, Hausel’s sandbox embeds AI agents inside a verification architecture and a human-directed workflow from the start, so that speed and scale are gained without sacrificing the certainty on which mathematics depends. If the bridge between representation theory and equivariant topology can be built this way, with an important result already proved and the research area coming into focus, the sandbox may demonstrate that the most productive future for AI in mathematics is not the lone machine genius of popular imagination but a disciplined collaboration, in which human taste sets the destination and machine-checked reasoning paves the road.

Subject of Research: AI-assisted mathematical proof verification and human-AI collaboration in representation theory and equivariant topology

Article Title: A mathematical universe in a sandbox | ISTA mathematician secures computational support for AI-assisted research

Article References: A mathematical universe in a sandbox | ISTA mathematician secures computational support for AI-assisted research. (n.d.). Original publication

Image Credits: AI Generated

DOI: Not provided

Keywords: Tamás Hausel, Project Numina, Project Sandbox, proof assistants, AI agents, representation theory, equivariant topology, machine-checked proofs, ISTA, formal mathematics, computer algebra oracle, human-AI collaboration