Cet article présente un deuxième tournant pour les machines dans le processus de découverte mathématique. Grâce à la vérification automatisée des preuves, les machines sont désormais capables d'automatiser la création de concepts mathématiques . Nous abordons l'état actuel de l'art, les obstacles, les solutions potentielles et les premières tentatives de formalisation mathématique de la création de concepts. Enfin, nous évaluons comment cette capacité pourrait transformer les mathématiques et la collaboration homme-machine, ainsi que certains scénarios futurs possibles.