🔢 mathematics

A sharp 5/8 bound for an Erd\H{o}s-Sós pairwise-sums problem

Cet article résout le problème 865 d'Erdős en prouvant que la taille minimale $f_3(N)$ requise pour qu'un sous-ensemble de $\{1,\dots,N\}$ contienne trois éléments distincts dont les sommes deux à deux sont également dans l'ensemble est exactement $5N/8 + O(1)$ , établissant ainsi une borne exacte qui correspond à une construction connue.

Auteurs originaux : Ricky Cipollini

Publié 2026-06-30

📖 4 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Ricky Cipollini

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 : La règle des « trois équipes »

Imaginez que vous organisiez une fête avec des invités numérotés de 1 à $N$ . Vous voulez inviter autant de personnes que possible, mais vous avez une règle très stricte : vous ne pouvez pas avoir trois invités (appelons-les Alice, Bob et Charlie) tels que si vous les associez par paires, leurs « nombres combinés » soient également des invités à la fête.

Par exemple, si Alice est la n°2 et Bob est le n°3, leur somme est 5. Si le n°5 est aussi à la fête, c'est un problème. La règle dit : vous ne pouvez pas avoir un trio où chaque paire possible (Alice+Bob, Alice+Charlie, Bob+Charlie) donne un nombre qui est également un invité de la fête.

Les mathématiciens appellent cela un « triple de sommes par paires ». Le papier pose une question simple : quel est le nombre maximum de personnes que vous pouvez inviter à cette fête avant d'être forcé de créer accidentellement l'un de ces trios interdits ?

La réponse : Le seuil des 5/8

Le document résout un puzzle célèbre (Problème d'Erdős 865) en prouvant une limite précise.

Considérez le nombre total d'invités ( $N$ ) comme une pizza géante. Le document prouve que si vous invitez plus de 5/8 de la pizza (plus une minuscule miette négligeable), vous ne pouvez pas éviter d'avoir un trio interdit.

La borne inférieure (la construction « mauvaise ») : Les auteurs montrent une manière spécifique d'inviter exactement 5/8 des invités sans enfreindre la règle. Ils font cela en invitant des personnes issues de deux tranches spécifiques de la pizza :
1. La tranche située de 1/8 à 1/4 du chemin.
2. La tranche située de 1/2 jusqu'à la fin.
  Si vous choisissez uniquement des personnes dans ces deux zones, leurs « sommes » ne retombent jamais dans la liste des invités. Cela prouve que vous pouvez atteindre 5/8.
La borne supérieure (la preuve « bonne ») : Le travail principal du document est de prouver que vous ne pouvez pas aller plus haut que 5/8. Si vous essayez d'inviter ne serait-ce qu'une personne de plus au-delà de ce seuil de 5/8, les mathématiques garantissent qu'un trio interdit apparaîtra.

Ainsi, la réponse est exactement 5/8. C'est une ligne de démarcation nette et précise.

Comment ils l'ont prouvé : L'astuce du « Pliage »

Pour prouver que vous ne pouvez pas aller plus haut que 5/8, les auteurs utilisent une astuce mentale ingénieuse appelée « Pliage » (Folding).

Imaginez que votre liste d'invités est une longue bande de papier.

Choisissez un Pivot : Choisissez un invité spécifique (appelons-le le « Pivot ») pour se tenir au milieu.
Pliez le Papier : Imaginez que vous pliez la bande de papier de sorte que les nombres en dessous du Pivot s'alignent avec les nombres au-dessus du Pivot.
- Si le Pivot est l'invité n°100, l'invité n°101 se replie sur le n°99, le n°102 sur le n°98, et ainsi de suite.
La Collision : Lorsque vous pliez le papier, certains nombres peuvent se retrouver l'un sur l'autre. Les auteurs analysent ce qui se passe lorsque ces nombres « pliés » interagissent.

Ils ont découvert que si vous avez trop d'invités, les nombres « pliés » créent une collision mathématique qui force l'existence d'un trio interdit. C'est comme essayer de faire entrer trop de valises dans une voiture ; finit par arriver un moment où la géométrie de la voiture force deux valises à s'entrechoquer.

La formalisation « Lean » (La vérification par le robot)

Le document mentionne qu'une partie de la preuve a été vérifiée par un programme informatique appelé Lean 4.

Considérez la preuve comme un pont complexe. Les auteurs l'ont construit à la main. Ensuite, ils ont remis les plans à un robot super précis (Lean) pour vérifier chaque boulon et chaque poutre. Le robot a confirmé que le pont est solide, sans fissures cachées ou moments de type « désolé, j'ai oublié une étape ». Cela donne à la communauté mathématique une confiance supplémentaire dans le fait que la limite de 5/8 est absolument correcte.

Résumé

Le Problème : Combien de nombres pouvez-vous choisir entre 1 et $N$ sans créer un « trio de sommes » spécifique ?
Le Résultat : Vous pouvez choisir jusqu'à 5/8 des nombres. Si vous en choisissez plus, vous êtes mathématiquement garanti de créer le trio.
La Méthode : Ils ont utilisé une technique de « pliage » pour montrer que toute tentative de dépasser cette limite provoque une contradiction logique.
La Signification : Cela résout un problème vieux de plusieurs décennies (Problème d'Erdős 865) et confirme que la limite de « 5/8 » est la meilleure réponse possible.

Résumé Technique : Une Borne Précise de 5/8 pour un Problème de Sommes Par Paire d'Erdős–Sós

Énoncé du Problème
L'article traite d'un cas spécifique de la conjecture d'Erdős–Sós concernant les sommes par paire. Soit $f_3(N)$ le plus petit entier tel que tout sous-ensemble $A \subseteq \{1, \dots, N\}$ avec $|A| \geq f_3(N)$ contient des éléments distincts $a, b, c \in A$ satisfaisant la condition que leurs sommes par paire $a+b$ , $a+c$ , et $b+c$ sont toutes contenues dans $A$ . Un tel ensemble est dit « exempt de triple de sommes par paire » si aucun tel triple n'existe. Le problème central est de déterminer le comportement asymptotique de $f_3(N)$ .

Avant ce travail, une construction standard $A = [\frac{N}{8}, \frac{N}{4}] \cup [\frac{N}{2}, N]$ démontrait que $f_3(N) \geq \frac{5}{8}N + O(1)$ . L'objectif de l'article est de prouver la borne supérieure correspondante, résolvant ainsi le Problème 865 d'Erdős et établissant la constante asymptotique exacte.

Méthodologie
La preuve est autonome et repose sur une combinaison d'induction combinatoire, de théorie additive des nombres et d'une technique de « pliage » (folding). La méthodologie procède à travers les étapes clés suivantes :

Le Lemme d'Addition Plié (Lemme 2.1) :
Les auteurs établissent d'abord un lemme sur un intervalle « plié ». Pour un ensemble $B \subseteq \{1, \dots, m-1\}$ où aucune paire distincte ne somme à $m$ ou à un autre élément de $B$ (modulo $m$ ), le lemme limite la taille de $B$ par rapport à l'ensemble des « collisions » $C(B)$ . Plus précisément, il prouve que $|B| - |C(B)| \leq \frac{m}{4} + 2$ . La preuve utilise la symétrie de réflexion ( $B \to -B$ ) et un argument inductif sur $|B|$ , en analysant les cas où la somme des deux plus petits éléments appartient à $C(B)$ ou non.
Le Lemme de Pliage (Lemme 3.1) :
Les auteurs introduisent une opération de « pliage » autour d'un élément pivot $h \in A$ . En partitionnant l'ensemble $A$ en éléments plus petits que $h$ ( $X$ ) et en éléments de la forme $h+r$ où $r < h$ ( $Y$ ), ils relient la taille de $A$ à la structure de l'intersection $B_h = X \cap Y$ . Le lemme démontre que si $A$ est exempt de triple, la somme des tailles $|X| + |Y|$ est bornée par $\frac{5}{4}h - |E \setminus C(B_h)| + 1$ , où $E$ représente les « lacunes » de l'intervalle $[1, h-1]$ . Cette étape réduit efficacement le problème de la borne de la taille globale de l'ensemble à l'analyse des propriétés additives locales modulo $h$ .
Borne Supérieure Inductive (Section 4) :
Le théorème principal est prouvé par induction forte sur $H$ (où $N=2H$ ). La preuve se divise en deux cas basés sur l'écart entre le plus grand élément de la moitié inférieure de l'intervalle et le plus petit élément de la moitié supérieure :
- Cas 1 ( $s \leq 4e$ ) : L'ensemble est plié autour du pivot $h = q$ (le plus petit élément de la partie supérieure). Les auteurs montrent que l'écart entre la partie inférieure et la partie supérieure de $A$ impose un nombre suffisant d'éléments « manquants » ( $|E \setminus C(B_h)|$ ) pour satisfaire la borne.
- Cas 2 ( $s > 4e$ ) : L'ensemble est plié autour de $h = p$ (le plus grand élément de la partie inférieure). Ici, le grand écart implique que la partie inférieure de l'ensemble est creuse. Les auteurs appliquent l'hypothèse d'induction au segment inférieur et combinent cela avec le lemme de pliage pour dériver la borne.

Contributions Clés et Résultats

Borne Supérieure Précise : L'article prouve que pour tout $N$ , tout sous-ensemble $A \subseteq [1, N]$ avec $|A| \geq \frac{5}{8}N + C$ (pour une certaine constante absolue $C$ ) contient un triple de sommes par paire.
Résolution du Problème 865 d'Erdős : En combinant la nouvelle borne supérieure avec la construction de borne inférieure existante, l'article établit que $f_3(N) = \frac{5}{8}N + O(1)$ . Cela confirme que la constante $5/8$ est la meilleure possible.
Formalisation : Les auteurs notent qu'une version conditionnelle antérieure de la réduction d'une borne plus grossière vers la borne précise a été formalisée dans Lean 4/Mathlib. Cette formalisation n'utilise aucun « sorry » (espace réservé) ni axiome ajouté, vérifiant la validité logique des étapes de réduction.
Conjecture Affinée : L'article mentionne une formule conjecturale plus précise suggérée par Stijn Cambie concernant la taille maximale exacte pour des $N$ spécifiques modulo 8, bien que le résultat principal demeure la borne asymptotique de $5/8$ .

Signification
L'article affirme résoudre le Problème 865 d'Erdős en fournissant une preuve autonome de la borne précise de $5/8$ . Sa signification réside dans la fermeture de l'écart entre la construction connue et la limite théorique supérieure pour ce problème spécifique de sommes par paire. Le travail est présenté comme une preuve mathématique complète, avec la rigueur supplémentaire d'une réduction formalisée en Lean, garantissant la validité des arguments combinatoires sans dépendre d'hypothèses non vérifiées. Les auteurs déclarent explicitement que la preuve est autonome et que toutes les constantes implicites sont absolues.