🔢 mathematics

Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof

Cet article présente la première résolution par une IA entièrement autonome du problème n° 728 d'Erdős, utilisant une combinaison de GPT-5.2 Pro et du système Aristotle pour générer une preuve formelle en Lean démontrant un phénomène d'écart logarithmique dans la divisibilité factorielle à travers une analyse inédite des coefficients binomiaux premier par premier.

Auteurs originaux : Nat Sothanaphan

Publié 2026-01-27

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Nat Sothanaphan

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

La vue d'ensemble : Une équipe de mathématiciens IA

Imaginez un célèbre génie des mathématiques à la retraite, Paul Erdős, qui a passé sa vie à laisser derrière lui une gigantesque liste de tâches (« To-Do list ») de puzzles non résolus. L'un de ces puzzles, le n° 728, est resté intact depuis des décennies.

Récemment, une équipe composée d'une IA super-intelligente (GPT-5.2 Pro) et d'un robot spécialisé dans la vérification mathématique (Aristote) l'a enfin résolu. Ils ne se sont pas contentés de deviner la réponse ; ils ont construit une preuve rigoureuse, étape par étape, qu'un ordinateur peut vérifier comme étant 100 % correcte. Les auteurs de ce document ne font que traduire ce code informatique en une histoire que les humains peuvent lire.

Le Puzzle : L'équilibre des factorielles

Le problème pose une question sur les factorielles (des nombres comme $5! = 5 \times 4 \times 3 \times 2 \times 1$ ).

Imaginez que vous avez un énorme tas de blocs représentant $n!$ . Vous voulez voir si vous pouvez construire deux tours plus petites, $a!$ et $b!$ , ainsi qu'une troisième petite tour $k!$ , de telle sorte que les deux petites tours s'insèrent parfaitement dans la grande sans qu'il ne reste aucun bloc.

Mathématiquement, cela signifie : Est-ce que $a! \times b!$ divise uniformément $n! \times k!$ ?

Le puzzle demande : Quelle peut être la taille de l'« écart » ( $k$ ) ?

Si $k$ est minuscule, il est facile de faire entrer les blocs.
Si $k$ est énorme, c'est généralement impossible.
L'astuce consiste à trouver une « zone Goldilocks » (une zone idéale) où $k$ est assez grand pour être intéressant, mais pas trop grand pour que les blocs ne puissent plus entrer.

L'équipe d'IA a prouvé que vous pouvez trouver une infinité de situations où cet écart ( $k$ ) est approximativement de la taille du logarithme du nombre total. En langage courant : si votre nombre total de blocs est d'un million, l'écart peut être d'environ 14. Si votre nombre est d'un milliard, l'écart peut être d'environ 20. Cela croît très lentement, mais cela croît.

La Stratégie : Le jeu des « retenues »

Pour résoudre cela, les mathématiciens ont dû examiner le problème à travers le prisme des nombres premiers (2, 3, 5, 7, etc.). Ils ont utilisé une règle appelée le Théorème de Kummer, qui est comme un jeu de « retenues » lors d'une addition.

L'analogie : Le seau qui déborde
Imaginez que vous additionnez des nombres dans une langue spécifique (base $p$ ).

Lorsque vous additionnez deux chiffres et que le résultat est trop grand pour un emplacement, vous « reportez » l'excédent à l'emplacement suivant (une retenue).
L'Objectif : L'IA devait trouver un nombre ( $m$ ) qui, lorsqu'il est doublé, provoque beaucoup de retenues (comme un seau qui déborde de façon répétée).
L'Obstacle : En même temps, l'IA devait s'assurer que les nombres qui suivent immédiatement $m$ (comme $m+1, m+2...$ ) ne présentent pas de « pics » — c'est-à-dire une divisibilité soudaine et massive par un nombre premier qui briserait l'équilibre.

Voyez cela comme une marche sur une corde raide :

La Corde Raide (la condition de « retenue ») : Vous devez choisir un nombre qui est « riche en retenues ». Quand vous le doublez, il doit faire déborder ses seaux aussi souvent que possible. Cela crée un « filet de sécurité » de divisibilité qui aide l'équation à fonctionner.
Les Pics (la condition « mauvaise ») : Vous devez éviter les nombres où les entiers suivants sont divisibles par de puissances énormes d'un nombre premier. Ce sont des « pics » qui pourraient vous faire tomber de la corde raide.

Comment ils ont trouvé la solution

L'IA n'a pas simplement choisi un nombre au hasard. Elle a utilisé un argument de comptage (une stratégie statistique) :

La zone de recherche : Ils ont examiné une immense plage de nombres (de $M$ à $2M$ ).
Le filtre : Ils ont calculé combien de nombres dans cette plage étaient « mauvais » (soit ils ne généraient pas assez de retenues, soit ils présentaient un pic).
Le résultat : Ils ont prouvé que le nombre de candidats « mauvais » est en réalité plus petit que le nombre total de candidats dans la plage.
La conclusion : Puisqu'il y a plus de nombres que de nombres « mauvais », il doit y avoir au moins un nombre « bon » restant dans le tas.

C'est comme dire : « Si vous avez un bocal de 1 000 billes, et que seulement 900 d'entre elles sont rouges (mauvaises), il doit en rester au moins 100 bleues (bonnes). » L'IA a prouvé que pour tout bocal suffisamment grand, une bille « bonne » existe toujours.

Pourquoi cela importe (selon le papier)

Première preuve uniquement par IA : C'est la première fois qu'un système d'IA résout de manière autonome l'un des célèbres problèmes d'Erdős et produit une preuve formelle que les humains peuvent vérifier.
L'« écart logarithmique » : Ils ont confirmé que l'écart entre les nombres peut être logarithmique. Bien que le papier note que l'écart pourrait potentiellement être légèrement plus grand (comme suggéré par le mathématicien Terence Tao), cette preuve établit une base solide et garantie.
Méthodologie : La méthode utilisée (compter les retenues et éviter les pics) est similaire aux techniques qu'Erdős lui-même utilisait par le passé, mais appliquée ici à une cible plus complexe et mouvante.

Résumé

Le document est un rapport sur la manière dont une équipe d'IA a résolu un puzzle mathématique vieux de 40 ans. Ils ont montré que l'on peut toujours trouver un ensemble spécifique de nombres où une équation factorielle complexe s'équilibre parfaitement. Ils y sont parvenus en traitant les nombres comme des seaux qui débordent (retenues) et en prouvant que l'on peut toujours trouver un seau qui déborde juste assez pour être utile, sans pour autant trop renverser de l'eau aux mauvais endroits.

Résumé Technique : Résolution du Problème d'Erdős #728

Énoncé du Problème
Le document traite du problème d'Erdős #728, qui étudie la taille maximale possible de l'écart $k := a + b - n$ sous la contrainte de divisibilité factorielle :
$a! b! \mid n! (a + b - n)!$
Sans contraintes supplémentaires, des solutions triviales existent où $k$ peut être arbitrairement grand (par exemple, en prenant $a$ et $b$ très grands). Pour rendre le problème non trivial, les auteurs imposent la condition que $a$ et $b$ soient éloignés des extrêmes, spécifiquement $\varepsilon n \le a, b \le (1-\varepsilon)n$ pour un certain $0 < \varepsilon < 1/2$ . L'objectif est de déterminer à quel point $k$ peut être grand par rapport à $n$ sous ces contraintes.

Méthodologie et Stratégie de Preuve
La preuve procède en transformant la condition de divisibilité factorielle en un problème concernant les coefficients binomiaux et les valuations $p$ -adiques.

Réduction à la Divisibilité Binomiale :
En posant $n = 2m$ , $b = m$ , et $a = m + k$ , la condition originale est équivalente à :
$\binom{m+k}{k} \mid \binom{2m}{m}$
Cela nécessite de montrer que pour chaque nombre premier $p$ , la valuation $p$ -adique du côté gauche est inférieure ou égale à celle du côté droit :
$\nu_p\left(\binom{m+k}{k}\right) \le \nu_p\left(\binom{2m}{m}\right)$
Analyse de la Valuation via le Théorème de Kummer :
En utilisant le théorème de Kummer, $\nu_p\left(\binom{2m}{m}\right)$ est identifié au nombre de retenues survenant lors de l'addition de $m + m$ en base $p$ . Le terme $\nu_p\left(\binom{m+k}{k}\right)$ est borné par la valuation maximale de n'importe quel terme dans le bloc consécutif $m+1, \dots, m+k$ , notée $V_p(m, k)$ .
L'inégalité centrale à satisfaire est :
$V_p(m, k) \le \kappa_p(m)$
où $\kappa_p(m)$ est le nombre de retenues pour $m+m$ en base $p$ .
Analyse par Nombre Premier :
Les auteurs divisent l'analyse en deux régimes basés sur la taille du nombre premier $p$ par rapport à $k$ :
- Grands Premiers ( $p > 2k$ ) : Dans cette plage, l'inégalité est automatiquement vérifiée. Puisque la longueur de l'intervalle $k$ est plus petite que $p/2$ , au plus un nombre dans le bloc $m+1, \dots, m+k$ peut être divisible par $p$ . Si une puissance élevée $p^J$ divise un terme, les chiffres en base $p$ de $m$ forcent au moins $J$ retenues lors de leur doublement, satisfaisant ainsi la condition.
- Petits Premiers ( $p \le 2k$ ) : Il s'agit de la difficulté principale. Les auteurs emploient un argument de comptage probabiliste pour trouver un entier $m$ $m$ dans un grand intervalle $[M, 2M]$ $[M, 2 M]$ qui satisfait simultanément deux conditions pour tous les $p \le 2k$ $p \leq 2 k$ :
  - Riche en retenues (Carry-Rich) : L'expansion en base $p$ de $m$ possède de nombreux chiffres $\ge \lceil p/2 \rceil$ dans les $L_p$ premières positions. Cela force un grand nombre de retenues ( $\kappa_p(m)$ ) lors du doublement de $m$ .
  - Sans pics (Spike-Free) : Aucun entier dans le bloc $m+1, \dots, m+k$ n'est divisible par une puissance de $p$ inhabituellement élevée (spécifiquement, $V_p(m, k)$ est maintenu sous un seuil $J_p + t(M)$ ).
Existence via l'Inégalité de Boole (Union Bound) :
Les auteurs définissent des ensembles « mauvais » d'entiers $m$ qui échouent soit à la condition de retenue, soit à la condition de pic. En utilisant les bornes de Chernoff pour la distribution des grands chiffres et un comptage simple pour la condition de pic, ils montrent que la mesure totale de ces mauvais ensembles est strictement inférieure à la taille de l'intervalle $[M, 2M]$ . Par conséquent, un $m$ « bon » existe qui satisfait la condition de divisibilité pour tous les nombres premiers pertinents simultanément.

Résultats Clés
Le document établit le Théorème 1 (Fenêtre d'écart logarithmique) :
Pour toutes constantes $0 < C_1 < C_2$ et $0 < \varepsilon < 1/2$ , il existe une infinité de triplets $(a, b, n) \in \mathbb{N}^3$ tels que :

$\varepsilon n \le a, b \le (1-\varepsilon)n$
$a! b! \mid n! (a + b - n)!$
$C_1 \log n < a + b - n < C_2 \log n$

La construction produit un écart $k$ qui croît de manière logarithmique avec $n$ . Les auteurs notent que la preuve actuelle produit $k \asymp \log n$ , mais que la méthode pourrait potentiellement être étendue à $k = \exp(c\sqrt{\log n})$ avec des raffinements supplémentaires, bien que la rédaction actuelle se concentre sur le régime logarithmique.

Signification et Revendications

Premier Problème d'Erdős résolu par une IA : Les auteurs affirment qu'il s'agit du premier problème d'Erdős « entièrement résolu de manière autonome par un système d'IA ». Le système utilisé était une combinaison de GPT-5.2 Pro et du prouveur de théorèmes « Aristotle » de Harmonic.
Vérification Formelle : La preuve a été générée sous forme de preuve formelle dans le prouveur de théorèmes Lean, puis traduite en mathématiques informelles présentées dans ce compte rendu.
Contribution Méthodologique : Ce travail étend les techniques antérieures d'Erdős et Pomerance concernant les diviseurs des coefficients binomiaux centraux. Contrairement aux travaux précédents qui se concentraient sur les entiers « pauvres en retenues » (peu de retenues) ou sur des tailles d'écart fixes, cette preuve construit des entiers « riches en retenues » pour gérer une fenêtre croissante de taille $k \asymp \log n$ .
Indépendance : Les auteurs notent qu'après leurs travaux initiaux, Carl Pomerance a dérivé indépendamment des résultats similaires, et que des modifications de cet argument ont été utilisées pour résoudre les problèmes d'Erdős #729 et #401.

Le document ne prétend pas résoudre le problème dans sa forme absolument la plus forte (notant le potentiel pour des écarts plus grands), mais affirme la résolution réussie de la question spécifique de l'écart logarithmique posée par Erdős.