J'ai personnellement franchi une ligne, et je suis un peu en admiration. C'est ma première preuve entièrement automatisée, générée par un LLM et auto-formalisée d'un nouveau théorème mathématique. Laissez-moi poser le problème : nous avons trois cercles rotatifs avec six positions chacun, tous trois s'intersectant en un total de six points. Prouvez que le groupe de mouvements qu'ils génèrent est le groupe symétrique complet S_{12}. C'est un problème que j'ai remarqué à l'origine dans un joli puzzle du jeu Machinarium par Amanita Design. La tâche n'est pas extrêmement difficile, mais elle a apparemment deux preuves : 1. Une recherche par force brute sur les classes de conjugaison pour représenter toutes les transpositions (j'ai fait cela il y a de nombreuses années mais je ne l'ai jamais publié). 2. Une preuve générée par un LLM (dans ce cas produite il y a environ trois mois par GPT-5-Pro), ou en fait deux preuves, utilisant toutes deux de manière brillante un théorème de Jordan sur les groupes primitifs (ou une variante étroitement liée qui est encore plus directe). ( Ce qui me manquait jusqu'à ce soir, c'était un outil pour auto-formaliser cette preuve. Grâce à @HarmonicMath, j'ai eu accès à leur logiciel remarquable, Aristotle. En résumé, voici ce que j'ai fait : A. J'ai auto-généré la preuve avec un LLM (et l'ai exécutée plusieurs fois pour obtenir une version beaucoup améliorée). B. J'ai réduit la preuve au texte mathématique de base—définitions, propositions, lemmes, théorèmes—avec des preuves fournies par le LLM. C. J'ai fait fonctionner le système Aristotle toute la nuit (via API). Ce matin, j'ai reçu une version entièrement formalisée en Lean (environ 700 lignes de code). Le code compile, donc j'ai maintenant un certificat confirmant que la preuve générée par le LLM a effectivement conduit à une solution correcte. De plus, j'ai obtenu une preuve conceptuelle, meilleure que ma propre force brute. Je prévois de pousser cela plus loin vers une classe plus large de tels problèmes algébriques. C'est un petit projet, mais pour moi personnellement, cela marque une étape importante. J'ai maintenant des outils qui, avec mon orchestration, peuvent vraiment m'aider à découvrir, formaliser et étudier des preuves de théorèmes mathématiques. Ce n'est pas trivial. Questions : 1. Comment cela va-t-il évoluer à l'avenir ? 2. Combien de formation sera nécessaire pour réussir de telles tâches ?...