Tamás Hausel, professeur à l’Institut des sciences et technologies d’Autriche (ISTA), a obtenu une bourse du Project Numina, une organisation à but non lucratif basée à Paris qui développe une intelligence artificielle libre pour les mathématiques. Elle comprend un soutien en calcul et un accès à des logiciels d’une valeur de 50 000 euros sur 12 mois.
Le projet, baptisé Sandbox, est un environnement numérique où mathématiciens et agents d’IA travaillent ensemble dans un domaine des mathématiques encore jamais formalisé dans un assistant de preuve. L’objectif est de bâtir une nouvelle théorie pour démontrer une famille de conjectures ouvertes, chaque étape étant vérifiée par ordinateur sous la direction de l’humain.
Un oracle de calcul formel vérifie les énoncés et un noyau de preuve certifie les démonstrations. Selon l’ISTA, le système fonctionnait en trois semaines et l’équipe a déjà démontré un résultat important.
