Squarefree numbers in short intervals: explicit and formalized

Imaginez la droite numérique comme une autoroute infinie et chatoyante qui s'étire vers l'horizon. Sur cette route, certains nombres sont « sans carré » (squarefree), ce qui signifie qu'ils sont construits à partir de blocs de construction uniques qui ne se répètent jamais. Imaginez-les comme un ensemble de briques LEGO où aucune pièce n'a la même couleur ; vous ne pouvez pas construire une tour carrée parfaite avec elles. Les mathématiciens savent depuis longtemps que si l'on observe une immense étendue de cette autoroute, ces nombres spéciaux apparaissent avec un rythme prévisible, environ 6 places sur 10. Mais que se passe-t-il si l'on zoome pour regarder un segment très court, minuscule, de la route ? Les nombres sans carré conservent-ils leur rythme, ou deviennent-ils chaotiques et imprévisibles ? C'est la question des « nombres sans carré dans des intervalles courts ». C'est un casse-tête dans le domaine de la théorie des nombres, une branche des mathématiques qui étudie les motifs cachés des nombres entiers. Résoudre cela aide à comprendre la structure fondamentale des mathématiques, un peu comme comprendre comment une seule brique s'insère dans un mur massif.

Dans cet article, Mayank Pandey s'attaque à ce casse-tête en prenant un résultat mathématique connu et en le rendant « explicite » et « formalisé ». Auparavant, un résultat existait qui prouvait que ces nombres se comportent bien dans des intervalles courts, mais il reposait sur un outil puissant et complexe (impliquant des « nilsequences » et les travaux de Green et Tao) qui agissait comme une boîte noire : il disait que la réponse était là, mais ne donnait pas les nombres spécifiques nécessaires pour la calculer. Le travail de Pandey est comparable au fait de démonter cette boîte noire, de mesurer chaque engrenage et chaque ressort à l'intérieur, et d'en écrire les dimensions exactes. Il prouve que si l'on choisit un point de départ $X$ qui est au moins aussi grand que $e^{1027/\varepsilon^2}$ (un nombre vertigineux) et que l'on regarde un intervalle de longueur $H = X^{1/5 - 2/90935 + \varepsilon}$, le nombre de nombres sans carré que l'on trouve sera très proche de la quantité attendue. Plus précisément, la différence entre le compte réel et le compte attendu est garantie d'être non plus grande que $10450 \varepsilon H X^{-\varepsilon/1025}$. C'est une promesse concrète et calculable, à condition que l'intervalle ne soit pas trop court et que le nombre de départ soit suffisamment grand.

Pour y parvenir, Pandey a dû naviguer dans un paysage délicat de « termes d'erreur », qui sont les petits vacillements dans le décompte. Il décompose le problème en différentes zones. Dans certaines zones, les vacillements sont faciles à dompter en utilisant des techniques standards, comme la soustraction répétée de différences pour lisser les bosses. Dans d'autres zones, plus difficiles, les vacillements sont tenaces. Dans l'article original, ces zones tenaces étaient gérées par l'outil de la « boîte noire » mentionné précédemment. Pandey, cependant, a décidé de faire le gros du travail manuellement. Il traite les expressions mathématiques comme un nœud de cordes emmêlées. Au lieu d'utiliser un tour de magie pour dénouer le nœud, il tire délicatement sur des brins spécifiques (en utilisant une méthode appelée « différer de van der Corput ») pour le desserrer. Il montre que même si les cordes semblent désordonnées, elles ne s'emmêlent pas de manière à ruiner le motif. En divisant le problème en cas plus petits et en les vérifiant un par un, il prouve que les « vacillements » sont assez faibles pour être ignorés dans son intervalle spécifique.

L'article fait également le choix délibéré de simplifier l'explication par souci de clarté. Bien que le code informatique (formalisé en Lean 4) contienne une version mathématique légèrement plus optimisée et précise, la note écrite présente une version « plus brute » qui est plus facile à suivre. C'est comme montrer à un étudiant une carte simplifiée d'une ville pour lui enseigner les principaux itinéraires, plutôt que de lui donner une image satellite avec chaque ruelle marquée. L'auteur note que cette simplification affaiblit légèrement l'exposant final, mais que la conclusion centrale reste solide : le motif des nombres sans carré tient bon même dans des intervalles très courts, et nous avons maintenant les chiffres exacts pour le prouver. Son travail est une preuve rigoureuse, et non une supposition ou une simulation, confirmant que la structure mathématique est aussi ordonnée que nous l'espérions, même lorsque nous l'observons à travers un microscope.