Ramanujan Machine : défi IA pour les preuves mathématiques
L'initiative Ramanujan Machine lance un défi inédit pour mesurer les capacités des systèmes d'intelligence artificielle à résoudre des problèmes mathématiques de niveau recherche. Intitulé Ramanujan Challenge, ce concours invite les participants à démontrer des formules relatives à des constantes mathématiques fondamentales telles que pi, e, la constante de Catalan ou certaines valeurs de la fonction zêta de Riemann. Ces problèmes sont conçus pour être vérifiables numériquement avec une précision arbitraire, tout en exigeant des raisonnements mathématiques subtils. Le défi se déroulera du 1er juillet au 1er août 2026 à 23h59 UTC. Les organisateurs souhaitent tester si l'IA peut générer des preuves rigoureuses sans recourir à des vérifications chaotiques. Pour garantir la reproductibilité, les soumissions sont classées par ordre de priorité : preuves formelles validées par des prouveurs interactifs comme Lean ou Coq, dérivations assistées par ordinateur utilisant des systèmes symboliques publics disponibles avant le lancement, ou démonstrations classiques lisibles par un humain. Tout code fourni doit être commenté, exécutable et soumis avec un fichier explicatif au format PDF ou TEX. Les règles mettent l'accent sur la transparence et l'intégrité scientifique. Les participants peuvent échanger publiquement sur les problèmes, mais il leur est interdit de diffuser leurs solutions complètes avant la date limite. Les programmes développés spécifiquement pour le concours sont autorisés comme outils de calcul, mais ne peuvent en aucun cas faire office de source de vérité ou contourner les étapes de vérification. Les APIs privées ou services cachés sont strictement interdits. Après la clôture des inscriptions, le comité évaluera chaque proposition, distinguant les preuves valides des contributions partielles, et identifiera les outils ou modèles utilisés. Toute démonstration acceptée concernant une conjecture ouverte sera reconnue comme une contribution mathématique nouvelle, avec attribution des crédits selon l'ordre de soumission. Ce projet s'inscrit dans une démarche visant à établir un standard de vérification structuré pour l'IA appliquée aux sciences exactes, tout en encourageant la transparence et la reproductibilité dans la recherche assistée par machine.
