🔢 mathematics

Kernel-Checked Exclusions for the Erdős-Selfridge Odd Covering Problem: Any Odd Covering of ℤ Has lcm Exceeding 10000

Cet article présente une formalisation en Lean 4 entièrement vérifiée par le noyau, prouvant que tout recouvrement fini des entiers par des moduli impairs distincts supérieurs à 1 doit posséder un plus petit commun multiple excédant 10 000, établissant ainsi une exclusion mécaniquement certifiée pour le problème du recouvrement impair d'Erdős-Selfridge sans recourir à des solveurs computationnels non vérifiés.

Auteurs originaux : Ibrahim Mian, Shayaan Siddique

Publié 2026-07-29✓ Author reviewed ⓘ

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Ibrahim Mian, Shayaan Siddique

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 par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez les entiers (les nombres entiers comme 1, 2, 3, et ainsi de suite) comme une autoroute infinie s'étendant dans les deux directions. Dans le monde des mathématiques, il existe un casse-tête fascinant sur la façon de « couvrir » cette autoroute. Un système de couverture est comme une équipe de gardes de sécurité, chacun stationné à un endroit spécifique et assigné à un schéma de patrouille. Par exemple, un garde pourrait vérifier chaque 2ème maison, un autre chaque 3ème maison, et un troisième chaque 4ème maison. Si vous les alignez correctement, leurs itinéraires de patrouille se chevauchent de telle sorte que chaque maison de l'autoroute infinie est visitée par au moins un garde. Les mathématiciens savent depuis des décennies qu'il est possible de faire cela, mais il y a un piège : dans tous les exemples connus, au moins un des gardes possède un schéma de patrouille « pair » (comme vérifier toutes les 2 ou 4 maisons).

Cela mène à une question tenace qui hante les mathématiciens depuis plus de 70 ans : est-il possible de couvrir toute l'autoroute en utilisant uniquement des gardes avec des schémas de patrouille « impairs » (comme toutes les 3, 5 ou 7 maisons), où aucun des deux gardes n'a la même taille de schéma ? C'est ce qu'on appelle le problème de la couverture impaire d'Erdős–Selfridge. C'est un peu comme demander si vous pouvez carreler un sol en utilisant uniquement des carreaux de forme impaire sans jamais utiliser un seul carreau de forme paire. Bien que nous ne connaissions pas encore la réponse finale, ce nouvel article agit comme un inspecteur ultra-précis et infaillible aux robots. Il ne résout pas tout le mystère, mais il prouve avec une certitude absolue que si un tel système de couverture entièrement impair existe, les nombres impliqués doivent être incroyablement grands — bien plus grands que ce que quiconque avait été capable d'exclure auparavant avec un ordinateur qui ne fait pas d'erreurs.

La découverte de l'article : Une zone d'exclusion protégée par les robots

Cet article, écrit par Ibrahim Mian et Shayaan Siddique, ne prétend pas avoir trouvé la solution au problème de la couverture impaire. Au lieu de cela, il construit une « forteresse numérique » pour prouver que toute solution potentielle doit être beaucoup plus grande que 10 000. Pensez au problème comme à un immense verrou dont la combinaison est faite de nombres. Les auteurs voulaient savoir : « La combinaison pourrait-elle être petite, comme 945 ou 1 200 ? » Leur réponse est un « Non » définitif, mais avec une touche très spéciale : ils n'ont pas seulement utilisé une calculatrice ; ils ont utilisé un robot mathématique (un programme informatique appelé Lean 4) pour vérifier chaque étape de leur logique, garantissant qu'aucune erreur humaine ou hypothèse cachée ne s'est glissée dans le processus.

Voici comment ils ont procédé, en utilisant quelques métaphores créatives :

1. Le piège de la densité (Le comptage de la foule)
D'abord, les auteurs ont examiné la « densité » des gardes. Si vous avez un groupe de gardes avec des tailles de patrouille impaires différentes, vous pouvez calculer quelle partie de l'autoroute ils couvrent. Pour qu'ils couvrent tout, leur couverture combinée doit atteindre 100 %. Les mathématiques montrent que pour que cela se produise avec des nombres impairs, le « plus petit commun multiple » (PPCM) — qui est comme la longueur totale du motif répétitif avant qu'il ne recommence — doit être un type de nombre très spécial appelé « abondant ». Un nombre abondant est un nombre où la somme de ses diviseurs (les nombres qui le divisent uniformément) est supérieure au nombre lui-même. C'est comme un nombre qui est si populaire que ses amis, une fois additionnés, valent plus que lui.

2. Le contrôle du plancher (La barrière de 945)
Les auteurs ont prouvé que le plus petit nombre impair qui est « abondant » est 945. Cela signifie que si un système de couverture entièrement impair existe, sa longueur de motif doit être au moins de 945. Tout ce qui est plus petit est mathématiquement impossible. C'était la première marche de leur échelle, un fait qu'ils ont vérifié avec une vérification informatique qui a pris environ 80 secondes de calcul pur et ininterrompu.

3. Les certificats de capacité (Le test de chevauchement)
C'est ici que la magie opère. Savoir simplement que les nombres sont « abondants » ne suffit pas ; vous devez aussi vérifier si les gardes s'emboîtent réellement sans laisser de vides. Les auteurs ont créé des « certificats de capacité ». Imaginez essayer de faire entrer des pièces de puzzle dans une boîte. Même si les pièces semblent devraient s'y ajuster, il arrive parfois qu'elles se chevauchent trop ou laissent de minuscules trous. Les auteurs ont écrit un test spécifique pour chaque nombre abondant impair inférieur à 10 000. Ils ont demandé : « Si nous essayons de construire un système de couverture en utilisant ces nombres impairs spécifiques, est-ce que les espaces entre les gardes deviennent trop grands pour être comblés ? »

Pour chaque nombre abondant impair inférieur à 10 000 (il y en a exactement 23), le test a répondu « Non, c'est impossible ». Les espaces étaient trop grands, ou les chevauchements étaient trop désordonnés. L'ordinateur a vérifié cela pour les 23 nombres, prouvant qu'aucun d'eux ne pouvait être la combinaison secrète.

4. Le verdict final (La limite de 10 000)
En combinant ces étapes, les auteurs ont prouvé un théorème majeur : Tout système de couverture des entiers utilisant des modules impairs distincts supérieurs à 1 doit avoir un plus petit commun multiple (PPCM) supérieur à 10 000.

En termes plus simples : si quelqu'un prétend avoir trouvé un moyen de couvrir l'autoroute infinie en utilisant uniquement des modèles de patrouille à nombres impairs, il ment si son motif se répète tous les 10 000 pas ou moins. Le motif doit être plus long que 10 000.

Pourquoi cela importe (Même si ce n'est pas la réponse finale)

Vous pourriez vous demander : « Et alors ? Ils ont juste prouvé que le nombre doit être plus grand que 10 000. Nous le savions déjà, c'est difficile. » Les auteurs sont très honnêtes à ce sujet : ils n'ont pas résolu tout le problème. La réponse réelle pourrait être un nombre comme 100 000 ou un milliard. Cependant, la manière dont ils l'ont fait est la véritable percée.

Habituellement, lorsque les mathématiciens utilisent des ordinateurs pour vérifier de longues listes de nombres, ils s'appuient sur des logiciels de type « boîte noire » qui peuvent contenir des bugs ou des hypothèses cachées. Cet article est différent. Ils ont construit tout leur argument à l'intérieur d'un « noyau de preuve » (proof kernel) — un cœur minuscule et fiable d'un programme informatique qui vérifie chaque étape logique comme un comptable paranoïaque. Ils n'ont utilisé aucun raccourci « magique » ou code non vérifié. Ils ont même prouvé que leur code informatique fonctionne correctement en le testant contre des exemples connus (comme le système de couverture classique de 12 étapes) pour s'assurer qu'il ne disait pas accidentellement « impossible » quand quelque chose était en réalité possible.

Ils ont également créé un pont qui relie le monde infini de tous les entiers au monde fini des vérifications informatiques. Cela signifie que dans le futur, si quelqu'un lance une recherche par supercalculateur pour trouver une solution, cet article fournit un moyen de vérifier les résultats sans faire confiance aveuglément à l'ordinateur.

L'essentiel

L'article exclut la possibilité d'un « petit » système de couverture impair. Il dit : « Si la réponse existe, elle se cache quelque part au-delà de 10 000. » Il ne nous dit pas où se trouve la réponse, mais il a dégagé tout le quartier des nombres inférieurs à 10 000 avec un niveau de certitude qu'aucun humain ne pourrait jamais atteindre seul. C'est un « Non » rigoureux et vérifié par robot aux petits nombres, laissant le mystère ouvert pour les grands, mais avec un nouvel outil inébranlable pour vérifier les découvertes futures.

Résumé technique : Exclusions vérifiées par le noyau pour le problème de couverture impaire d'Erdős–Selfridge

Énoncé du problème
L'article traite du problème de la couverture impaire d'Erdős–Selfridge (problème n°7 d'Erdős), qui demande s'il existe un système de couverture des entiers $\mathbb{Z}$ où tous les modules sont impairs, distincts et supérieurs à 1. Un système de couverture est une famille finie de classes de congruence $a_i \pmod{n_i}$ dont l'union est $\mathbb{Z}$ . Bien qu'il soit établi que tout système de couverture existant avec des modules distincts $>1$ contient au moins un module pair, l'existence d'une variante exclusivement impaire demeure un problème ouvert.

Méthodologie
Les auteurs présentent une formalisation en Lean 4 (utilisant mathlib) qui établit une exclusion vérifiée par le noyau : toute couverture de $\mathbb{Z}$ par des modules impairs distincts $>1$ doit avoir un plus petit commun multiple (PPCM) des modules supérieur à 10 000. La stratégie de preuve évite le calcul non vérifié ou les solveurs externes dans la base de confiance, en s'appuyant sur une chaîne de cinq étapes formalisées :

Argument de densité : Les auteurs formalisent l'argument de la sagesse populaire selon lequel si un système de couverture utilise des modules distincts divisant $N$ (tous $>1$ ), la somme de leurs réciproques doit être au moins égale à 1. Cela implique que $2N \le \sigma_1(N)$ , ce qui signifie que $N$ doit être un nombre parfait ou abondant.
Réduction au PPCM : Pour toute couverture de $\mathbb{Z}$ , la preuve réduit le problème au PPCM ( $L$ ) des modules. Puisque les modules sont distincts et impairs, $L$ doit être un nombre impair, non déficient (parfait ou abondant).
Plancher d'abondance : Un calcul vérifié par le noyau confirme que le plus petit nombre abondant impair est 945. Par conséquent, toute couverture de ce type doit avoir un PPCM $\ge 945$ .
Certificats de capacité : Pour exclure des candidats spécifiques, les auteurs formalisent une borne de « capacité de reste chinois ». Cette inégalité arithmétique décidable tient compte des chevauchements entre les classes de congruence avec des modules premiers deux à deux. Si les points « non couverts » restants après la prise en compte de ces chevauchements ne peuvent pas être couverts par les diviseurs restants de $N$ $N$ , le système est prouvé impossible.
- Une « lemme de relaxation monotone » garantit qu'un certificat dérivé d'une famille complète de nombres premiers s'applique même si un système de couverture n'utilise qu'un sous-ensemble de ces modules.
- Cette étape génère un certificat pour chacun des 23 nombres abondants impairs inférieurs à 10 000, réfutant ces derniers comme valeurs potentielles de PPCM.
Énumération : Un évaluateur de somme de diviseurs à carburant constant (sigma100) est implémenté pour éviter l'inefficacité des mécanismes généraux de diviseurs lors de la réduction du noyau. Cela permet au noyau de vérifier que les 23 nombres abondants impairs inférieurs à 10 000 sont les seuls candidats dans cette plage.

Contributions clés
La principale contribution de l'article est épistémique plutôt que mathématique, se concentrant sur la vérification rigoureuse d'arguments élémentaires connus au sein d'un assistant de preuve formelle :

Théorème principal : Une preuve vérifiée par le noyau qu'une couverture de $\mathbb{Z}$ par des modules impairs distincts $>1$ a un PPCM $> 10 000$ .
Certificats de capacité formalisés : Une inégalité décidable, par- $N$ , dérivée de bornes de comptage du CRT, qui réfute les couvertures pour des $N$ spécifiques, accompagnée d'un lemme garantissant que ces certificats s'appliquent à n'importe quelle sous-famille de modules.
Énumération vérifiée par le noyau : Une preuve que la liste des 23 nombres abondants impairs inférieurs à 10 000 est complète, utilisant un évaluateur spécialisé conçu pour la réduction du noyau.
Pont formel : Une traduction bidirectionnelle entre la formulation concrète du système de couverture utilisée dans la preuve et la structure StrictCoveringSystem définie dans le dépôt google-deepmind/formal-conjectures. Cela garantit que l'exclusion s'applique à la définition abstraite du problème, et non seulement à des exemples concrets.
Méthodologie de porte d'axiome (Axiom-Gate) : Le développement limite strictement sa base de confiance à exactement trois axiomes (propext, Classical.choice, Quot.sound). Il exclut explicitement sorry, native_decide et les solveurs externes, avec des vérifications CI automatisées confirmant qu'aucun axiome supplémentaire n'est introduit.

Résultats

La formalisation exclut avec succès tous les nombres abondants impairs $N < 10 000$ comme valeurs de PPCM possibles pour un système de couverture impair.
La preuve établit que si un système de couverture impair existe, son PPCM doit être au moins de 10 001.
La méthode montre une limite stricte aux nombres « traînards » 10 395, 12 285 et 17 325, qui ne sont pas exclus par les certificats de capacité actuels.
Le système de couverture classique de période 12 est vérifié pour satisfaire tous les hypothèses des lemmes de densité, tandis que l'arithmétique de capacité échoue correctement à l'exclure (car il s'agit d'une couverture valide), servant ainsi de contrôle de cohérence.

Signification et affirmations
Les auteurs déclarent explicitement que ce travail ne résout pas le problème d'Erdős–Selfridge, ni n'améliore les limites mathématiques existantes (par exemple, la classification de McNew et Setty jusqu'à $10^6$ ). Au lieu de cela, la signification réside dans :

Certitude épistémique : Transformer des arguments d'exclusion élémentaires en théorèmes du noyau de Lean, éliminant la dépendance à l'égard de la littérature non formalisée ou des pipelines de calcul non vérifiés.
Modèle méthodologique : Fournir un cadre réutilisable pour les « certificats de capacité » et un modèle pour convertir les exclusions par- $N$ en certificats décidables traités par decide.
Intégration future : Établir un « pont de périodicité bidirectionnel » entre les couvertures de $\mathbb{Z}$ et les vérifications finies sur $\mathbb{Z}/N\mathbb{Z}$ . Cela permet à de futures recherches mécaniques (telles que les solveurs SAT ou les énumérations exhaustives) de produire des résultats qui peuvent être consommés et vérifiés par le noyau, plutôt que de faire confiance directement à la sortie du solveur.

L'article conclut que bien que l'exclusion à 10 000 ne règle pas la question ouverte, elle fournit une fondation vérifiée et un « socle » portable pour de futures recherches certifiées sur le problème.

La découverte de l'article : Une zone d'exclusion protégée par les robots

Pourquoi cela importe (Même si ce n'est pas la réponse finale)

L'essentiel

Articles similaires