Récemment, un groupe de chercheur de Google a déclaré avoir créé une Intelligence artificielle destinée à prouver des théorèmes mathématiques. Pour cela, ils ont développé un outil basé sur HOL Light Theorem Prover, un logiciel capable de formaliser et de vérifier des raisonnements mathématiques. Dans la première phase de conception, l’IA a été entrainée à résoudre 10,200 théorèmes dont la majorité traite sur l’algèbre linéaire, l’analyse réelle ou l’analyse complexe. Malgré le fait que cette IA constitue une innovation dans le domaine de la mathématique expérimentale, l’équipe de Google a souligné que cet outil pourra être exploité dans différentes applications.
Les résultats de la phase d’entrainement de l’IA ont été concluants d’après les chercheurs. Pendant cette période, l’outil a pu prouver 5,919 des théorèmes proposés, soit 58% de bonnes réponses. Lors de la phase d’application, les chercheurs de Google lui ont soumis une série de 3,217 nouveaux théorèmes qui ne lui ont pas été enseignés. Malgré cela, l’IA a quand même été capable de prouver 1,251 théorèmes, soit 38,9% de taux de réussite. De nos jours, les outils mathématiques basés sur l’Intelligence artificielle sont nombreux. Dernièrement, des scientifiques ont développé une nouvelle formule pour calculer Pi, une expression simplifiée de la formule sommatoire d’Euler ainsi que de nouveaux résultats au problème de la somme des cubes de Mordell.
