Project Sandbox builds interconnected laboratories for mathematics — sandboxes — where we explore and develop theories with AI agents through reasoning, computation and verification. A human mathematician sets the research agenda and judges which results matter; the AI agents build the tools, compute, formulate conjectures, attempt proofs and review one another’s work. Nothing enters the record until a computer algebra oracle has vetted the statement and a proof kernel has certified the proof.

One family, three marks

almanac: a sandbox’s published record; the pilot, almanacA0a, shows the form.
Open Sandbox, the open mark: the reusable software, the same way of working, opened to everyone.
Project Sandbox, the closed mark: the research environment, a contained place to experiment.

The colours say how a result is known: ink for a refereed proof, orange for a computation, blue for a proof checked by machine.

What is public

• Open Sandbox, the reusable software: a folder in which you do mathematical research with AI agents, in the computer algebra system of your choice, and which can start or join a collab with other mathematicians’ sandboxes. It runs on Linux, macOS and Open Math OS.
  git.ista.ac.at/ai-for-mathematics/open-sandbox.
• almanacA0a, the pilot almanac: not a research result, but the smallest case, the centre of the even hybrid family quantum GL(1), run through the whole way of working to see how a sandbox’s record can be published. Every statement in it carries its warrant, and the edition explains how to check all of it yourself. DOI 10.5281/zenodo.22808194 · read it online · GitHub · GitLab.
• The story: A mathematical universe in a sandbox, ISTA News, 8 October 2026.
• The eyepiece: the interactive viewer of GKM graphs of affine Grassmannians in the Zoo.
• Talks, made with the assistance of SandboxHQ:
  • From Hitchin systems to quantum groups, the Hitchin80 conference, Madrid, Oct 2026.
  • Pólya, GKM and Macdonald in the centre of a quantum group, Erdős Center, Budapest, Nov 2026.

The first campaign

The first campaign connects two areas of mathematics, representation theory and equivariant topology. In the words of the ISTA story: “The project 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 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.”

Directed by

Tamás Hausel at the Institute of Science and Technology Austria (ISTA).

Supported by

A Project Numina Fellowship and the ERC Advanced Grant ViaFiPoS, No. 101199663.

Funded by the European Union. Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council Executive Agency. Neither the European Union nor the granting authority can be held responsible for them.