L’équipe FAIR de Meta a publié six articles de recherche détaillant comment ses modèles d’IA ont permis de résoudre six problèmes mathématiques ouverts dans divers domaines. Parmi les résultats les plus concrets, une conjecture formulée par García-Martínez et Pérez-Rodríguez sur les algèbres résolubles a été réfutée grâce à la contribution centrale de l’IA. Le système AutoformBot a par ailleurs formalisé en Lean 4 un total de 26 manuels de mathématiques, produisant une bibliothèque de plus de 45 000 déclarations et des centaines de milliers de lignes de code vérifié. Meta insiste sur le fait que l’IA accompagne les mathématiciens sans les remplacer, les humains conservant le choix des questions, l’interprétation des résultats et la rédaction des preuves. L’utilisation de systèmes de vérification formelle comme Lean permet de confirmer de manière irréfutable que les preuves générées par l’IA tiennent effectivement debout.
Source: Lire l’article original
