Project Sandbox builds interconnected laboratories for mathematics — sandboxes — where we explore and develop theories with AI agents through reasoning, computation and verification.
How it works
A mathematician sets the research agenda and judges which results matter. 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.
The three colours of the marks stand for three kinds of evidence in mathematics:
Use
- Open Sandbox
A folder in which you do mathematical research with AI agents, in the computer algebra system of your choice. It can start or join a collab with other mathematicians’ sandboxes, and runs on Linux, macOS and Open Math OS. - almanacA0a
The pilot almanac: a toy sandbox published whole — explanation, informal proof, Julia instrument, Lean proof, and a concordance across all three.
Results
The first project connects representation theory and equivariant topology. It tests whether AI agents can help build a proof-producing bridge between them: from quantum groups and the Langlands classification to affine Schubert varieties and GKM graphs.
- GKM viewer
An interactive viewer of GKM graphs of affine Grassmannians.
Talks
Media
Collaborators
- Shiyu Shen, ISTA
- Fernando Rodriguez-Villegas, ICTP
- Aleksandr Zhabin, ISTA
- András Szenes, University of Geneva
- Tamás Hausel, ISTA