🔢 mathematics

Dead ends in square-free digit walks

Cet article démontre que la densité asymptotique des « impasses » dans les marches de chiffres sans facteur carré est d'environ $1,317 \times 10^{-9}$ , ce qui est environ 40 000 fois plus petit que ce qui est prédit par les modèles stochastiques, et établit une expression sous forme fermée pour ces densités dans toutes les bases en utilisant un résultat entièrement formalisé dans Lean/Mathlib par le système AxiomProver.

Auteurs originaux : Evan Chen, Chris Cummins, Ben Eltschig, Dejan Grubisic, Leopold Haller, Letong Hong, Andranik Kurghinyan, Kenny Lau, Hugh Leather, Seewoo Lee, Aram Markosyan, Ken Ono, Manooshree Patel, Gaurang Pendha

Publié 2026-02-09

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Evan Chen, Chris Cummins, Ben Eltschig, Dejan Grubisic, Leopold Haller, Letong Hong, Andranik Kurghinyan, Kenny Lau, Hugh Leather, Seewoo Lee, Aram Markosyan, Ken Ono, Manooshree Patel, Gaurang Pendharkar, Vedant Rathi, Alex Schneidman, Volker Seeker, Shubho Sengupta, Ishan Sinha, Jimmy Xin, Jujian Zhang

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

Le Jeu : « La Marche des Chiffres Sans Carré »

Imaginez que vous jouez à un jeu avec des nombres. Vous commencez avec un nombre qui est « sans carré ».

Qu'est-ce qu'un nombre sans carré ? C'est un nombre qui ne contient aucun carré parfait caché en lui comme facteur (autre que 1). Par exemple, 10 est sans carré (c'est $2 \times 5$ ), mais 12 ne l'est pas (c'est $4 \times 3$ , et 4 est un carré).
Le Mouvement : Vous essayez de « marcher » vers l'infini en ajoutant un chiffre à la fois à la fin de votre nombre. Si vous avez le nombre 5, vous pouvez essayer de créer 50, 51, 52, ..., jusqu'à 59.
La Règle : Chaque nouveau nombre que vous créez doit également être sans carré. Si vous créez un nombre qui n'est pas sans carré, ce chemin spécifique est une « impasse ».

La Grande Question : Pouvez-vous continuer à marcher éternellement ? Existe-t-il un nombre de départ et une séquence de chiffres que vous pouvez choisir pour ne jamais heurter une impasse, vous permettant ainsi de marcher vers l'infini ?

L'Ancienne Hypothèse : « La Théorie du Pile ou Face »

Avant ce papier, des mathématiciens (spécifiquement Miller et al.) ont étudié ce problème en utilisant un modèle « stochastique » ou aléatoire. Ils traitaient la propriété d'être sans carré comme un lancer de pièce.

Environ 60 % de tous les nombres sont sans carré.
Ils imaginaient que pour chaque étape franchie, vous aviez 6 de chances de trouver un chiffre « sûr » à ajouter.
Comme vous avez 10 chiffres à disposition, ils ont calculé que les probabilités de rester bloqué (heurter une impasse) étaient très faibles.
Leur Prédiction : Ils pensaient que les impasses étaient rares, survenant environ 52 fois tous les millions de nombres. Ils croyaient que les marches infinies étaient presque garanties.

La Nouvelle Découverte : « Le Piège Arithmétique »

Ce papier prouve que la « Théorie du Pile ou Face » est fausse. Le monde réel des nombres est bien plus obstiné qu'un simple lancer de pièce aléatoire.

Les auteurs (un mélange d'humains mathématiciens et d'un outil d'IA appelé AxiomProver) ont découvert que les impasses sont en réalité extrêmement rares — environ 1 sur un milliard.

Pourquoi cette différence ?
Le modèle « Pile ou Face » supposait que les raisons pour lesquelles un nombre échoue sont indépendantes. Il pensait qu'échouer à cause du chiffre '0' n'avait rien à voir avec le fait d'échouer à cause du chiffre '1'.

En réalité, les règles de l'arithmétique créent un piège serré.

L'Analogie : Imaginez essayer de verrouiller une porte avec 10 clés différentes. L'ancienne théorie pensait que chaque clé avait 60 % de chances de fonctionner de manière indépendante.
La Réalité : Les « serrures » (les carrés de nombres premiers comme $4, 9, 25, 49$) sont très exigeantes. Pour qu'un nombre échoue pour les 10 chiffres à la fois, il doit satisfaire un ensemble de conditions très spécifiques et complexes impliquant simultanément de nombreux nombres premiers différents.
Parce que ces conditions sont si spécifiques et interdépendantes, il est incroyablement difficile de trouver un nombre qui échoue pour chaque chiffre suivant possible. Les « impasses » sont si rares que le modèle aléatoire a largement surestimé leur fréquence.

Le Résultat : Une Nouvelle Formule

Le papier fournit une formule mathématique précise (une « expression de forme fermée ») pour calculer exactement la rareté de ces impasses pour n'importe quelle base (pas seulement la base 10).

Pour la base 10, la véritable densité des impasses est d'environ $1,3 \times 10^{-9}$ .
C'est environ 40 000 fois plus petit que la prédiction précédente.

La Touche « IA » : AxiomProver

Une partie unique de ce papier est la manière dont les mathématiques ont été réalisées.

Les auteurs n'ont pas seulement rédigé la preuve à la main. Ils ont utilisé un outil d'IA appelé AxiomProver.
Ils ont soumis à l'IA une description en langage clair du problème : « Trouver la densité des impasses dans les marches de chiffres sans carré. »
L'IA ne s'est pas contentée de deviner ; elle a dérivé la formule et a écrit une preuve formelle dans un langage informatique appelé Lean.
L'ordinateur a ensuite vérifié la preuve étape par étape pour s'assurer qu'elle était 100 % correcte logiquement.
Les auteurs humains ont ensuite pris cette preuve générée par ordinateur et ont écrit ce papier pour l'expliquer à d'autres humains.

Une Note Historique (La « Mise à Jour »)

Le papier inclut une mise à jour importante : après avoir publié leurs travaux, ils ont appris qu'un mathématicien nommé Mirsky avait en fait résolu ce problème exact en 1947.

Le papier de 2024 de Miller et al. (qui a lancé le débat sur le « Pile ou Face ») avait oublié de citer les travaux de Mirsky de 1947.
Ainsi, bien que les mathématiques de ce papier soient correctes et que la preuve par l'IA soit une nouvelle prouesse technologique, le résultat lui-même n'est pas nouveau dans l'histoire des mathématiques. Les auteurs ont décidé de ne pas publier cela dans une revue car la réponse était déjà connue, mais ils partagent cela pour montrer l'efficacité de leur outil d'IA à redécouvrir les mathématiques anciennes.

Résumé

Le Jeu : Pouvez-vous ajouter des chiffres indéfiniment sans heurter un nombre qui n'est pas sans carré ?
L'Ancienne Vue : Oui, presque certainement. Les impasses sont rares (1 sur 20 000).
La Nouvelle Vue : Les impasses sont super rares (1 sur un milliard) car les règles des mathématiques sont plus strictes que le hasard.
La Méthode : Un outil d'IA nommé AxiomProver a réussi à dériver la formule correcte et à la prouver, redécouvrant un résultat de 1947 qui avait été oublié.

Résumé Technique : Impasses dans les marches de chiffres sans carrés

Énoncé du Problème
L'article étudie l'existence et la densité des « impasses » (dead ends) dans les marches de chiffres sans carrés. Une marche sans carrés en base $b$ commence par un entier sans carré $N_0$ et tente de construire une séquence infinie $N_0, N_1, N_2, \dots$ où chaque terme suivant est formé en ajoutant un chiffre $d \in \{0, \dots, b-1\}$ tel que $N_{k+1} = bN_k + d$ reste sans carré.

Un entier positif $N$ est défini comme une impasse si :

$N$ est sans carré.
Pour chaque chiffre $d$ de la base, l'extension $bN + d$ n'est pas sans carré.

La question centrale, posée par Miller et al. [5], est de savoir si des marches sans carrés infinies existent. Bien qu'un modèle stochastique (le « Modèle Aveugle Illimité ») suggère que des marches infinies existent avec une probabilité proche de 1 (impliquant que les impasses sont rares, avec une densité asymptotique de $\approx 5,218 \times 10^{-5}$ en base 10), cet article analyse rigoureusement la densité arithmétique réelle des impasses pour déterminer si la prédiction stochastique se vérifie.

Méthodologie
Les auteurs emploient une combinaison de théorie multiplicative élémentaire des nombres et de principes d'inclusion-exclusion, évitant les hypothèses probabilistes du modèle stochastique.

Fonctions Indicatrices : Le problème est reformulé à l'aide de la fonction de Möbius $\mu(n)$ . Puisque $\mu(n)^2$ est la fonction indicatrice des entiers sans carrés, l'indicateur d'une impasse $N$ est exprimé par :
$\mathbb{1}_{N \text{ est une impasse}} = \mu(N)^2 \prod_{d \in D} (1 - \mu(bN + d)^2)$
où $D$ est l'ensemble des chiffres.
Inclusion-Exclusion : Le terme produit est développé en une somme sur tous les sous-ensembles $S$ de l'ensemble des chiffres. Cela transforme la fonction de comptage $D_b(X)$ (le nombre d'impasses $\le X$ ) en une somme alternée de fonctions de comptage $Q_S(X)$ , où $Q_S(X)$ compte les entiers $n \le X$ tels que $n$ et toutes ses extensions $bn+d$ (pour $d \in S$ ) soient sans carrés.
Analyse par Crible : Pour un sous-ensemble $S$ fixé, la condition que $n$ et $bn+d$ soient sans carrés est analysée nombre premier par nombre premier. Les auteurs définissent des classes de résidus « mauvaises » modulo $p^2$ qui doivent être évitées. En utilisant le théorème des restes chinois, ils déterminent la densité des entiers évitant ces classes.
- Pour les grands nombres premiers $p$ (où $p \nmid b$ ), la condition $p^2 \mid (bn+d)$ force $n$ dans une classe de résidus unique modulo $p^2$ . Crucialement, un seul carré de nombre premier peut obstruer au plus une extension de chiffre à la fois.
- La densité est exprimée par un produit infini (produit d'Euler) de facteurs locaux $(1 - \nu_{p,b}(S)/p^2)$ , où $\nu_{p,b}(S)$ compte le nombre de classes de résidus interdites modulo $p^2$ .
Contrôle du Terme d'Erreur : La preuve borne soigneusement les termes d'erreur provenant de la troncature du crible à un paramètre $z$ et de la contribution des grands nombres premiers, établissant un terme d'erreur de $O(X/\sqrt{\log X})$ .

Résultats Clés

Théorème 1.1 (Base 10) : La densité asymptotique des impasses en base 10 existe et est donnée par :
$c_{\text{dead}} = \sum_{S \subseteq \{0,\dots,9\}} (-1)^{|S|} \prod_{p \text{ premier}} \left( 1 - \frac{\nu_p(S)}{p^2} \right)$
où $\nu_p(S)$ est le décompte des classes de résidus $n \pmod{p^2}$ telles que $p^2 \mid n$ ou $p^2 \mid (10n+d)$ pour un certain $d \in S$ .
La valeur calculée est $c_{\text{dead}} \approx 1,317 \times 10^{-9}$ .
Théorème - 1.2 (Base générale $b$ ) : Le résultat se généralise à toute base $b \ge 2$ . La densité $c_{\text{dead}}(b)$ est donnée par une expression similaire impliquant une somme alternée de produits d'Euler. L'article fournit des approximations calculées pour les bases premières $b \in \{2, 3, 5, 7\}$ .
Écart avec les Modèles Stochastiques : La densité réelle ( $\approx 1,3 \times 10^{-9}$ ) est environ 40 000 fois plus petite que la prédiction stochastique ( $\approx 5,2 \times 10^{-5}$ ). L'article attribue cela aux dépendances arithmétiques : le modèle stochastique naïf suppose l'indépendance entre les extensions de chiffres, mais en réalité, l'exigence que les dix extensions échouent simultanément nécessite l'obstruction simultanée par de nombreux carrés de nombres premiers distincts, une condition bien plus stricte que ce que suggère le modèle de probabilité indépendante.

Signification et Revendications

Résolution de Conjecture : L'article démontre que si l'heuristique stochastique prédit que les marches infinies sont presque certaines, la structure arithmétique réelle rend les impasses considérablement plus rares que prévu. Cependant, l'existence d'une marche infinie reste un problème ouvert ; l'article quantifie la rareté des « obstructions » (impasses) mais ne prouve pas l'existence d'un chemin infini.
Formalisation : Une revendication principale de l'article est que le théorème principal (Théorème 1.2) a été entièrement formalisé en Lean/Mathlib et que la preuve a été produite automatiquement par un outil d'IA nommé AxiomProver. Le système a reçu uniquement l'énoncé en langage naturel du problème et a dérivé de manière autonome la formule en forme fermée ainsi que la preuve.
Contexte Historique (Mise à jour) : Les auteurs notent qu'après la publication initiale sur arXiv, ils ont appris de Kannan Soundararajan que le résultat principal avait été obtenu précédemment par Mirsky en 1947 [6]. L'article reconnaît que le travail de 2024 par Miller et al. [5] a omis de référencer ce travail antérieur. Par conséquent, bien que la formalisation en Lean constitue une preuve automatisée valide, les auteurs déclarent que le manuscrit ne sera pas soumis pour publication dans une revue en tant que contribution de recherche primaire, servant plutôt d'étude de cas pour la preuve de théorèmes automatisée.

Conclusion
L'article fournit une dérivation arithmétique rigoureuse de la densité des impasses dans les marches de chiffres sans carrés, révélant un écart massif par rapport aux prédictions stochastiques dû aux dépendances de la théorie des nombres. Sa contribution la plus notable, telle que formulée par les auteurs, est la formalisation complète de bout en bout de ce résultat en utilisant AxiomProver, démontrant la capacité des systèmes d'IA actuels à traiter des problèmes non triviaux en théorie analytique des nombres.