Tamás Hausel, a professor at the Institute of Science and Technology Austria (ISTA), has received a fellowship from Project Numina, a Paris-based nonprofit developing open-source artificial intelligence for mathematics. The fellowship includes computing support and software access worth €50,000 over 12 months.
The project, called Sandbox, is a digital environment where mathematicians and AI agents work together in an area of mathematics not yet formalised in any proof assistant. The goal is to build a new theory to prove a family of open conjectures, with every step machine-checked under human direction.
A computer algebra oracle checks statements and a proof kernel certifies proofs. According to ISTA, the system was running within three weeks and the team has already proved one important result.
