Il y a une différence entre une IA qui résout plus rapidement des problèmes connus et une IA qui découvre quelque chose de véritablement nouveau. La première est impressionnante. La seconde change tout.
AxiomProver, le système d’Axiom, vient de franchir cette limite en résolvant la conjecture ouverte de Fel, un véritable problème de mathématiques qui attendait depuis longtemps dans la littérature scientifique que quelqu’un (ou quelque chose) le résolve.
Voici comment AxiomProver l’a réellement résolue
AxiomProver a reçu trois éléments en entrée : un document expliquant le problème en langage courant, une instruction en une ligne (« Énonce et démontre la conjecture de Fel en Lean »), ainsi que le système de vérification des preuves à utiliser.
D’abord, il a lu et compris le problème en déterminant quels objets mathématiques étaient concernés et ce qu’il fallait démontrer.
Ensuite, il a tout traduit en Lean, un langage de preuve qui joue le rôle d’un arbitre strict pour les mathématiques. Chaque étape logique doit être justifiée par des principes fondamentaux, et l’ordinateur vérifie que chacune est correcte. C’est comme disposer d’un vérificateur des faits qui repère la moindre erreur dans votre raisonnement.
La partie créative est ensuite arrivée : AxiomProver a choisi une stratégie de démonstration fondée sur les fonctions génératrices exponentielles, une technique qui transforme des structures complexes de mathématiques discrètes en fonctions continues plus faciles à manipuler, les transforme algébriquement, puis revient en arrière pour démontrer que la formule d’origine est bien vérifiée.
Imaginez cette technique comme la transformation de briques LEGO en pâte à modeler, que l’on peut remodeler plus facilement, avant de les reconvertir pour prouver que les briques s’assemblent parfaitement. Enfin, AxiomProver a exécuté la démonstration étape par étape dans Lean, chaque opération logique étant vérifiée par l’ordinateur. Résultat : une preuve complète et formellement vérifiée.
Pourquoi cela dépasse le cadre des mathématiques
Lorsque l’IA peut découvrir de nouvelles vérités mathématiques de manière autonome, elle est potentiellement capable de débloquer des avancées majeures dans la science des matériaux, la découverte de médicaments, l’informatique quantique et tous les domaines où des problèmes mathématiques non résolus constituent des goulots d’étranglement. En somme, les mathématiques sont au fondement de tout, de la cryptographie qui sécurise votre compte bancaire à la physique qui maintient les avions dans les airs.
Les mêmes techniques qu’utilise AxiomProver pourraient bientôt vérifier qu’un logiciel est fiable et résistant au piratage. Imaginez une IA capable de garantir mathématiquement que votre dispositif médical ne tombera pas en panne ou que le code de votre voiture autonome ne connaîtra aucune défaillance.
Note de la rédaction : ce contenu a d’abord été publié dans la newsletter de notre publication sœur, The Neuron. Pour lire d’autres articles de The Neuron, inscrivez-vous à sa newsletter ici.