Des chercheurs du MIT, dont David Roe ’06 et Andrew Sutherland ’90, doctorant en 2007, font partie des lauréats des premiers bourses AI for Math attribuées par Renaissance Philanthropy et XTX Markets. Ces subventions visent à accélérer la découverte mathématique grâce à l’intelligence artificielle. Quatre autres anciens étudiants du MIT — Anshula Gandhi ’19, Viktor Kunčak (master 2001, doctorat 2007), Gireeja Ranade ’07 et Damiano Testa (doctorat 2005) — ont également été récompensés pour des projets distincts. Les 29 projets sélectionnés soutiendront des mathématiciens et chercheurs dans des universités et organisations qui travaillent à développer des systèmes d’intelligence artificielle capables d’assister à l’avancement de la recherche mathématique dans des domaines clés. Roe et Sutherland, accompagnés de Chris Birkbeck de l’Université d’East Anglia, utiliseront leur financement pour renforcer la preuve automatique de théorèmes en établissant un lien entre la base de données L-Functions and Modular Forms Database (LMFDB) et la bibliothèque mathématique Lean4 (mathlib). « Les outils de preuve automatique sont très techniques, mais leur développement est mal financé », souligne Sutherland. Avec l’émergence des grands modèles linguistiques (LLM), la barrière d’accès à ces outils formels diminue rapidement, rendant les systèmes de vérification formelle accessibles aux mathématiciens en activité. Mathlib est une vaste bibliothèque communautaire de mathématiques conçue pour le système formel Lean, qui vérifie rigoureusement chaque étape d’un raisonnement. Elle contient actuellement environ 105 résultats mathématiques (lemmes, propositions, théorèmes). La LMFDB, quant à elle, est une ressource collaborative en ligne considérée comme une « encyclopédie » de la théorie des nombres moderne, avec plus de 109 énoncés concrets. Roe et Sutherland en sont les rédacteurs en chef. Pour surmonter ces défis, les chercheurs vont concevoir des outils permettant d’accéder à la LMFDB depuis mathlib, rendant ainsi une vaste base de connaissances mathématiques non formalisées accessible à un système de preuve formelle. Cette approche permet aux assistants de preuve d’identifier des cibles précises pour la formalisation, sans devoir formaliser l’intégralité de la LMFDB d’un coup. « Rendre disponible dans mathlib une base de données étendue de faits en théorie des nombres va constituer une puissante méthode de découverte mathématique, car l’ensemble des faits qu’un agent pourrait envisager lors de la recherche d’un théorème ou d’une preuve est exponentiellement plus vaste que l’ensemble des faits qui doivent réellement être formalisés pour prouver ce théorème », explique Roe. Les chercheurs soulignent que la démonstration de nouveaux théorèmes à la pointe des connaissances mathématiques repose souvent sur des calculs non triviaux. Par exemple, la preuve de Fermat par Andrew Wiles repose sur une technique connue sous le nom du « truc 3-5 ». En exploitant les résultats préalablement calculés, la LMFDB permet d’économiser des milliers d’années de temps de calcul, évitant ainsi de devoir répéter ces calculs. De plus, la disponibilité de ces données précalculées rend possible la recherche d’exemples ou de contre-exemples, même sans connaître à l’avance la portée de la recherche. Les bases de données mathématiques sont aussi des référentiels soigneusement sélectionnés, pas des collections aléatoires. « Le fait que les théoriciens des nombres aient mis l’accent sur le rôle du conducteur dans les bases de données sur les courbes elliptiques a déjà été déterminant dans une découverte majeure réalisée à l’aide d’outils d’apprentissage automatique : les murmurations », note Sutherland. « Nos prochaines étapes consistent à constituer une équipe, à collaborer avec les communautés LMFDB et mathlib, à commencer à formaliser les définitions sous-jacentes aux sections sur les courbes elliptiques, les corps de nombres et les formes modulaires de la LMFDB, et à permettre des recherches dans la LMFDB directement depuis mathlib », conclut Roe. « Si vous êtes étudiant au MIT et intéressé par participer, n’hésitez pas à nous contacter ! »