Les grandes conjectures mathématiques reposent encore largement sur l’intuition d’experts. Dans un article publié sur arXiv, des chercheurs décrivent un cadre fondé sur les grands modèles de langage (LLM) pour systématiser, au moins en partie, la découverte et l’évaluation de nouvelles conjectures jugées prometteuses.
Le dispositif présenté s’organise en trois étapes. D’abord, une phase de recherche de régions s’appuie sur des modules d’évidence locale explicite pour faire émerger des pistes. Ensuite, une validation réflexive examine chaque proposition selon plusieurs critères, notamment son caractère fondamental, sa nouveauté et son importance potentielle. Enfin, une validation formelle est réalisée avec Lean 4 et Mathlib, afin de vérifier que les énoncés produits peuvent être correctement traduits et contrôlés dans un environnement de preuve.
L’objectif affiché n’est pas seulement de produire des problèmes difficiles, mais d’identifier des conjectures ayant ce que les auteurs appellent un fort "problem taste" : des énoncés dont une preuve pourrait restructurer le langage d’un domaine de recherche et offrir une aide durable aux mathématiciens. Cette ambition reste, à ce stade, programmatique, mais elle éclaire la direction du travail.
Sur le plan expérimental, l’article indique avoir testé vingt candidats. Selon le résumé, les vingt sur vingt passent l’analyse syntaxique et le contrôle de type dans Lean, ne sont pas directement résolus par `exact?`, et ne sont pas automatiquement déchargés par `aesop`. Les auteurs signalent aussi l’absence de doublons explicites ou quasi-doublons parmi ces propositions. À partir du seul résumé disponible, il reste toutefois difficile d’évaluer la profondeur mathématique réelle de ces conjectures ou leur portée au-delà de cette première démonstration de faisabilité.