- Le problème d’Erdős n°728 a récemment été résolu presque de manière autonome par des outils d’IA, marquant une nouvelle étape dans l’automatisation de la recherche en mathématiques
- Le problème était à l’origine une question sur la factorisation en nombres premiers des coefficients binomiaux posée en 1975 par Erdős, Graham, Ruzsa, Strauss, et il est longtemps resté difficile à traiter clairement en raison de conditions ambiguës
- ChatGPT a généré une preuve sous des contraintes ajustées, puis Aristotle l’a formalisée en preuve formelle Lean en corrigeant automatiquement les erreurs
- Plusieurs participants l’ont ensuite réécrite en langage naturel avec ChatGPT et ont amélioré de manière itérative une version renforçant les liens avec la littérature et la structure narrative
- Terence Tao estime que ce processus montre le potentiel de la capacité de l’IA à rédiger et corriger rapidement des preuves pour transformer la manière même d’écrire des articles de recherche
Le problème d’Erdős n°728 résolu par l’IA
- L’application récente d’outils d’IA a apporté de nouveaux progrès dans la résolution de problèmes d’Erdős, et le problème n°728 a été résolu presque de manière autonome par l’IA
- Après une première tentative, une version corrigée intégrant les retours a permis d’aboutir
- Le résultat n’a pas été reproduit à l’identique dans la littérature existante ; seuls des résultats proches par des méthodes similaires y figurent
- Ce cas montre que, ces derniers mois, les capacités de l’IA en résolution de problèmes mathématiques se sont réellement améliorées
- Par le passé, l’IA avait déjà été créditée de la résolution de problèmes d’Erdős, mais la plupart de ces résultats se sont ensuite révélés déjà présents dans la littérature
- Dans ce cas précis, l’énoncé original d’Erdős avait été présenté sous une forme incorrecte, et ce n’est que récemment qu’il a été reconstruit sous la forme voulue
- Cela expliquerait le manque de travaux antérieurs sur le sujet dans la littérature
Histoire du problème et premières approches
- En 1975, Erdős, Graham, Ruzsa, Strauss ont étudié la factorisation en nombres premiers du coefficient binomial (2n choose n) et ont posé plusieurs problèmes connexes
- L’un d’eux demandait s’il existe une infinité de a, b, n satisfaisant la condition a!b! | n!(a+b−n)! et a+b > n + C log n
- Cependant, plusieurs éléments, dont la taille de C (petite ou grande), étaient formulés de manière ambiguë
- Il y a quelques mois, l’équipe AlphaProof a trouvé une solution simple au problème, mais celle-ci ne correspondait pas à l’esprit du problème visé, ce qui a conduit à ajouter la contrainte a,b ≤ (1−ε)n
- Même après une recherche bibliographique assistée par IA, très peu de travaux pertinents ont été trouvés
Collaboration entre ChatGPT et Aristotle
- Le 4 janvier, ChatGPT a généré une preuve pour le cas de petit C sous les contraintes ajustées
- Cette preuve a ensuite été formalisée en preuve formelle Lean par Aristotle
- En réexaminant le texte original, il a toutefois été confirmé que l’article initial traitait déjà le cas du petit C
- Un autre participant a converti la preuve Lean en langage naturel avec ChatGPT, puis a produit une version améliorée au fil d’échanges supplémentaires
- Cette version comblait certaines lacunes de la démonstration, mais conservait encore une tournure maladroite typique de l’IA et un manque de références à la littérature
- Malgré cela, elle a atteint un niveau suffisamment lisible pour comprendre l’idée centrale
Réécriture à grande échelle et résultat amélioré
- Grâce à des prompts supplémentaires, ChatGPT a généré une preuve étendue jusqu’au cas de grand C
- Il subsistait quelques erreurs, mais Aristotle les a corrigées automatiquement et a achevé une preuve vérifiée par Lean
- Un troisième participant a compressé la preuve Lean, puis un autre, au terme d’une longue conversation avec ChatGPT, a
- réécrit le tout sous la forme d’un article abouti, avec des liens à la littérature et une structure narrative renforcés
- Le résultat a été jugé moins marqué par l’aspect typique d’un texte généré par IA, et d’une qualité proche de celle d’un article de recherche
- Tao indique avoir relu ce texte sur le forum consacré aux problèmes d’Erdős
Comment l’IA transforme la rédaction des articles de recherche
- Tao estime que, dans l’article final, les parties essentielles doivent encore être rédigées par des humains, mais
- l’association de l’IA et de Lean a, selon lui, considérablement accéléré la rédaction et la correction des preuves
- Jusqu’ici, rendre un article agréable à lire demandait beaucoup de temps, et
- les révisions à la suite des retours des relecteurs se limitaient souvent à des modifications locales
- Désormais, la combinaison de la génération et de la révision de texte par l’IA avec la vérification offerte par les outils de preuve formelle permet
- de produire rapidement de nouvelles versions d’un article avec différents niveaux de précision et de narration
- Au-delà d’un unique « article officiel », l’existence de nombreuses versions auxiliaires générées par l’IA
- ouvre la possibilité d’apporter des points de vue variés et une valeur supplémentaire
Réactions de la communauté
- Certains utilisateurs ont décrit la valeur ajoutée des documents générés par l’IA comme la capacité à voir les choses sous un autre angle
- D’autres mathématiciens ont souligné la nécessité de mesurer l’originalité des résultats produits par l’IA ou d’évaluer leur similarité avec la littérature existante
- Par exemple, une proposition consiste à mesurer quantitativement cette similarité en comparant la longueur des preuves formelles Lean
- Un autre commentaire avance que l’IA peut réécrire un article de manière globale, comme dans un refactoring de code, ce qui
- pousserait les chercheurs à se concentrer davantage sur la conception de la structure générale des documents
- Certains se sont montrés sceptiques quant à la possibilité que l’IA remplace le rôle des mathématiciens, mais
- d’autres y voient une nouvelle opportunité de collaboration et d’élargissement de la réflexion
1 commentaires
Réactions sur Hacker News
Je travaille chez Harmonic, et je voudrais corriger quelques malentendus au sujet d’Aristotle
Aristotle exploite activement des techniques d’IA de pointe, y compris la modélisation du langage
Si on lui fournit une preuve informelle en anglais, il a de fortes chances de la traduire en Lean si cette preuve est correcte. C’est donc un signal fort que la preuve en anglais est solide
Une fois formalisée en Lean, il n’y a plus de doute sur la validité de la preuve. C’est le cœur de notre approche — si une recherche pilotée par l’IA trouve une réponse, l’exactitude du résultat est garantie, quelle que soit sa complexité
Rust utilise un ensemble fixe de règles pour garantir la sûreté mémoire, mais ces règles sont simples et restrictives. Si un système comme Aristotle pouvait être intégré au compilateur, et qu’il laissait automatiquement passer le code lorsqu’une preuve de correction est possible, ce serait vraiment formidable
Je me demande combien de temps il faudra avant que Harmonic puisse formaliser la majorité des mathématiques écrites par des humains. Le concurrent Christian Szegedy dit que ce sera possible d’ici la fin de l’année
D’après l’explication de Terence Tao, un humain faisait circuler les résultats entre deux outils d’IA, et l’IA jouait le rôle de bouche-trou dans les lacunes trouvées par l’humain
Cela ressemble davantage à une collaboration entre humain et IA qu’à une résolution totalement autonome. En d’autres termes, un expert mène la danse et l’IA assiste
Recomposer des preuves existantes ou les combiner d’une manière nouvelle est un processus ennuyeux ou complexe pour les humains, mais l’IA peut le faire à une vitesse surhumaine
Cette approche pourrait ouvrir un potentiel énorme même avant l’AGI. On dirait qu’une époque arrive où les mathématiciens utiliseront l’IA comme outil pour s’attaquer à des problèmes aussi difficiles que les problèmes du millénaire
La vraie valeur des LLM réside dans leur capacité à proposer de nouvelles perspectives sur des sujets exprimables en langage
En lisant le billet explicatif de la personne qui a réellement résolu le problème, ce qui m’a frappé, c’est qu’ils ont obtenu le résultat avec seulement quelques prompts, sans énorme pipeline
Les modèles récents consomment bien plus de ressources de calcul, donc cela ressemble plutôt à une borne inférieure de performance qu’à une limite supérieure
Terence Tao a créé une page wiki intitulée « AI contributions to Erdős problems »
D’après la page GitHub et ce post sur Mathstodon, ce résultat (problème 728) est le premier « élément vert » de cette page, c’est-à-dire le premier cas effectivement résolu par l’IA
Je me demande si même les experts de domaines complexes comme la physique ou les mathématiques discutent avec des IA pour obtenir de l’aide
Si je classe par domaine, son utilité décroît dans l’ordre suivant : programmation > ML appliqué > statistiques/maths appliquées > maths pures
On peut essayer Aristotle directement dès maintenant — https://aristotle.harmonic.fun/
uvx aristotlelib@latest aristotle», mais en réalité il faut écrire «uvx --from aristotlelib@latest aristotle»De plus, le lien vers la page personnelle de Stanford est incorrect (il faut retirer
www)Ce résultat concerne un théorème sur les entiers, un domaine bien pris en charge par l’infrastructure Mathlib
Les définitions utilisées ne sont pas non plus complexes, donc ce type de preuve a de bonnes chances de réussir. Cela reste néanmoins une réussite vraiment impressionnante
C’est un exemple qui montre le potentiel d’une approche d’IA spécialisée au-delà des LLM
L’article sur Aristotle est disponible sur arXiv:2510.01346
Utiliser une architecture Transformer ne fait pas automatiquement de tout un LLM — si elle n’est pas entraînée sur des données linguistiques, on ne peut pas l’appeler un LLM
Autrement dit, toutes les étapes reposent sur des LLM
En 2026, l’IA semble devoir s’attaquer à de plus en plus de problèmes mathématiques non résolus
Ce cas n’était pas totalement autonome, mais après le feedback humain, l’IA est presque arrivée à une résolution par elle-même
À mon avis, le débat « les LLM ne sont que des perroquets stochastiques » est désormais terminé. La vraie discussion va désormais porter sur la manière de les mettre en pratique