Hexagone magique : trouvé avec l'IA pour toutes les tailles

L'énigme en nid d'abeilles a désormais une réponse pour toutes les tailles. L'auteur a trouvé la preuve avec l'aide de l'IA, et l'assistant de preuve Lean l'a vérifiée par machine ; une relecture indépendante reste à venir. Elle est expliquée ici sans jargon.

Un hexagone magique est un casse-tête numérique qui se joue sur des cases en nid d'abeilles. La preuve que de tels hexagones existent pour toutes les tailles a été trouvée avec l'aide de l'IA et vérifiée par machine par Lean. Cette démonstration automatisée a demandé quelques heures de calcul. Il s'agit bien ici de l'énigme mathématique, et non de la notion du même nom en politique économique.

L'article explique d'abord ce que l'énigme exige et retrace le parcours depuis le premier hexagone jusqu'à la preuve. Vient ensuite l'idée de la preuve en cinq étapes, chacune illustrée par une figure. La fin examine pourquoi on peut se fier à une preuve vérifiée par ordinateur, ce qu'un humain doit tout de même contrôler, et quels chiffres et faits se cachent derrière le résultat.

Hexagone magique : ce qu'exige le casse-tête numérique

La surface de jeu est une figure en nid d'abeilles en forme d'hexagone régulier. Sa taille s'appelle l'ordre n et indique combien de cases se trouvent sur un côté. Un hexagone d'ordre n compte 3n(n−1)+1 cases. Pour n = 3, cela fait 19 cases, pour n = 10 déjà 271.

On écrit des nombres entiers dans les cases, de sorte que chaque rangée droite donne la même somme. On compte les rangées dans les trois directions de la figure. Il y a 2n−1 rangées dans chaque direction. Les plus courtes, au bord, comptent n cases, la rangée centrale en compte 2n−1.

Le plus célèbre hexagone magique contient les nombres de 1 à 19 et a l'ordre 3. Chaque rangée donne 38. C'est l'hexagone classique, et avec les nombres à partir de 1, c'est la seule taille pour laquelle l'énigme fonctionne. Une simple considération de divisibilité montre que la somme de rangée nécessaire n'est un nombre entier que pour n = 1 et n = 3. Pour tous les autres ordres, la variante classique échoue donc dès le départ.

Le nouveau travail porte donc sur une variante voisine. Au lieu de commencer à 1, on utilise les nombres entiers de −K à K, chacun exactement une fois, avec K = 3n(n−1)/2. Pour n = 3, ce sont les nombres de −9 à 9, pour n = 10 les nombres de −135 à 135. Chaque rangée donne 0, et le 0 se trouve au centre.

L'énigme paraît anodine, mais elle est difficile. Le nombre de remplissages possibles croît si vite avec n qu'un essai systématique sur ordinateur ne mène pas loin. Il fallait donc un plan de construction valable pour toutes les tailles, et une preuve que ce plan fonctionne toujours.

De l'énigme de 1887 au plus grand hexagone connu : le parcours

Le problème d'origine vient d'Ernst von Haselberg et est généralement daté de 1887. Certaines sources indiquent 1888 ; la source primaire n'a pas été consultée. Plus tard, Adams a retrouvé l'hexagone classique en 1957, d'après son propre récit, et l'a fait connaître grâce à la rubrique de Martin Gardner. Charles W. Trigg a démontré, avec une publication en 1964, que cette solution est la seule, à rotation et symétrie près. L'université de Bielefeld tient une collection à ce sujet, et Wolfram MathWorld en donne un aperçu.

La variante avec des nombres entiers consécutifs et une somme de 0 est venue plus tard. Entre 2004 et 2006, les ordres 4 à 8 ont été trouvés : l'ordre 6 en octobre 2004, les ordres 7 et 8 en 2006. Jusqu'en 2006, seul l'ordre 8 était connu comme plus grande solution. Les ordres plus petits étaient alors déjà résolus. La Wikipédia allemande en donne un aperçu avec des références, mais certaines dates n'y sont pas sourcées.

En 2024, Dr. DSGVO, l'auteur de ce blog, a trouvé avec l'IA une solution d'ordre 9. C'était alors la plus grande solution connue.

Le 2 août 2026, Konstantin Gukov a publié un motif sur son site New magic hexagons. Il a cherché des solutions jusqu'à l'ordre 21 et a reconnu qu'on pouvait probablement en déduire une règle de construction pour des hexagones de n'importe quelle taille. Gukov a décrit à cet effet un algorithme et une esquisse de preuve censée s'appliquer à partir de l'ordre 114. Il souligne lui-même que cette esquisse n'est pas formalisée en Lean et n'a pas été vérifiée de façon indépendante. La preuve restait donc à faire.

Pour combler cette lacune, il existe désormais une preuve pour tous les ordres à partir de 3. Elle a été produite avec l'IA et est documentée dans une description du 21 octobre 2026. Lean l'a vérifiée par machine ; une relecture indépendante reste à venir, et les fichiers Lean ne sont pas encore liés publiquement. Nous y reviendrons.

Hexagones magiques pour toutes les tailles : ce qui est prouvé

Il est prouvé que, pour tout ordre n à partir de 3, il existe un hexagone magique avec les nombres de −K à K, dans lequel chaque rangée, dans les trois directions, a pour somme 0. La version renforcée, où le 0 se trouve en plus au centre, est elle aussi prouvée. Il n'y a pas de limite supérieure. L'esquisse de Gukov ne s'applique qu'à partir de l'ordre 114, les ordres précédents restaient ouverts sans la dernière étape.

La couverture est échelonnée. L'ordre 2 est impossible, car les sept nombres de −3 à 3 ne peuvent pas être répartis convenablement. Cette partie ne fait pas partie de la preuve Lean. Pour les ordres 3 à 6, il existe des hexagones tout faits, que Lean a revérifiés nombre par nombre. Pour les ordres 7 à 61, un plan de construction général s'applique, complété par une solution vérifiée d'un sous-problème pour chaque ordre. Pour les ordres 62 à 118, c'est la même chose, sauf que les listes nécessaires ont été recalculées et vérifiées. À partir de l'ordre 119, un plan de construction fixe suffit, prouvé de façon générale pour tout n.

Deux théorèmes principaux résument l'ensemble. Le premier affirme qu'il existe un hexagone magique d'ordre n pour tout n à partir de 3. Le second dit la même chose pour la version renforcée avec le 0 au centre. Les deux théorèmes n'ont d'autre hypothèse que n ≥ 3.

La preuve en cinq étapes : vue d'ensemble

On peut se représenter la preuve comme une échelle. Chaque étape réduit la tâche jusqu'à ce qu'il ne reste plus qu'un plan de table sur un banc. Les étapes 1 à 4 étaient déjà disponibles et vérifiées. La cinquième étape est nouvelle : le plan de table pour toutes les tailles. Elle clôt la preuve.

Les sections suivantes passent les étapes en revue l'une après l'autre. Les trois premières sont intuitives, les deux dernières peuvent être un peu plus techniques. Tous les calculs ont été vérifiés par Lean ; dans le texte, les idées suffisent donc.

Étape 1 : un sixième suffit, car en face se trouve l'opposé

Il n'est pas nécessaire de planifier tout l'hexagone, un sixième suffit. Chaque case a une case opposée, symétrique par rapport au centre. Si une case contient le nombre a, la case opposée reçoit −a. Chaque nombre est ainsi utilisé avec son opposé, et le 0 reste réservé au centre.

Cela a une conséquence pratique pour les rangées. La rangée symétrique a exactement la somme opposée. Si une rangée est équilibrée, son image miroir l'est aussi. Les rangées passant par le centre sont même équilibrées d'elles-mêmes.

Autour du centre, l'hexagone se décompose en six triangles identiques. Trois d'entre eux sont des triangles opposés : leurs nombres découlent de la symétrie par le centre avec le signe inversé. Deux autres sont des copies du sixième triangle tournées de 120 degrés et reçoivent des nombres étroitement liés. Il reste un seul triangle libre de T = n(n−1)/2 cases. Pour n = 10, ce sont 45 cases au lieu de 271.

La condition « chaque rangée a pour somme 0 » devient ainsi une condition sur ce triangle. Pour chaque rangée, une somme pondérée de ses entrées doit donner zéro. Cette somme s'appelle dans la suite le bilan de la rangée.

Étape 2 : chaque nombre devient base plus chiffre

La deuxième étape décompose chaque nombre en deux parties, une base et un chiffre. Les deux parties sont équilibrées séparément. Comme les sommes de rangées s'additionnent simplement, l'hexagone est magique dès que les deux parties sont équilibrées chacune de leur côté.

Pour cela, le stock de nombres de 1 à 3T est divisé en groupes de trois : k, T+k et 2T+k pour k de 1 à T. Chaque groupe est la base T+k plus T fois un chiffre, où le chiffre vaut −1, 0 ou 1. Pour l'hexagone d'ordre 3, T = 3 et le stock va de 1 à 9. La base 4 donne 1, 4 et 7, la base 5 donne 2, 5 et 8, la base 6 donne 3, 6 et 9.

La tâche se scinde ainsi en deux énigmes indépendantes. La première est un champ de chiffres composé de −1, 0 et 1 avec un bilan nul dans chaque rangée. La seconde est un champ de bases, où les valeurs absolues de T+1 à 2T sont réparties et munies de signes de sorte que le bilan de chaque rangée soit nul.

Étape 3 : le champ de chiffres grandit comme une échelle

Le champ de chiffres est entièrement résolu pour tout ordre à partir de n = 5, par récurrence par pas de trois. Le principe est celui de toute échelle : qui a le premier barreau et une règle pour passer au suivant atteint chaque barreau.

Il existe d'abord des champs de chiffres équilibrés tout faits pour les rayons 4, 5 et 6. Le rayon est ici n−1. Une règle d'extension s'applique ensuite : un champ de chiffres équilibré peut être agrandi de trois nouvelles couches au bord. Les nouvelles couches sont dessinées de sorte qu'elles s'annulent mutuellement dans chaque rangée. De 4, on passe ainsi à 7, 10, 13 et au-delà, de 5 à 8, 11 et au-delà, de 6 à 9, 12 et au-delà. Chaque rayon à partir de 4 est ainsi atteint.

Cette partie coûte à peine du temps de calcul lors de la vérification. Elle ne résout toutefois que la première des deux sous-énigmes ; le champ de bases reste ouvert.

Étape 4 : des écarts souhaités qui se compensent mutuellement

Le champ de bases n'est pas recherché directement. On fixe d'abord, pour chaque paire de cases, de combien ses deux bases doivent différer. Ces écarts souhaités sont prouvés de façon générale pour tous les ordres à partir de n = 13.

Presque toutes les cases du triangle forment des paires symétriques par rapport à son axe médian. L'une des cases d'une paire reçoit un moins, l'autre un plus. Dans le bilan, il ne reste alors que la différence des deux valeurs, la part commune T disparaît. Seul compte donc l'écart entre les deux rangs. Le rang est simplement le numéro de place : la base T+k a le rang k.

Les écarts souhaités se construisent en plusieurs étapes. Il y a des cycles d'associativité : de petits motifs de quatre paires de cases avec des poids +1 et −1 et un bilan nul dans chaque rangée. Le nom vient de la règle de calcul selon laquelle, dans une somme, on peut déplacer les parenthèses sans changer le résultat. Toute somme de tels motifs a elle aussi un bilan nul. De nombreux motifs naît un champ maître dans lequel aucune paire de cases n'obtient l'écart 0. Un écart 0 serait inutilisable, car deux cases ne peuvent jamais porter le même nombre.

Les cases de l'axe médian n'ont pas de partenaire. Elles reçoivent les plus petits rangs 1, 2, 3 et ainsi de suite, et le champ maître compense exactement leur contribution. Les cases diagonales portent en plus la part T, qui ne s'annule pas. Deux chaînes ramifiées de paires de cases, les forêts, la compensent. Leurs écarts sont augmentés d'environ T/2, soit T au total.

Le résultat est un jeu complet d'écarts souhaités avec un bilan nul dans chaque rangée, dont aucun n'est nul. La plupart des écarts sont petits et valent au plus 12. Les cases de la première ligne ont des écarts allant jusqu'à environ 2n, les paires des forêts des écarts proches de T/2.

Étape 5 : le plan de table pour toutes les tailles

Il faut enfin répartir réellement les rangs de 1 à T, de sorte que chaque paire de cases obtienne exactement son écart souhaité. À partir de n = 119, cela se fait avec un plan de construction fixe ; en dessous, avec des listes trouvées par ordinateur et vérifiées par Lean.

On peut se le représenter comme un plan de table sur un long banc de T places. Les cases diagonales sont assises à demeure sur les premières places 1, 2, 3 et ainsi de suite. Chaque paire de cases a besoin de deux places à l'écart prescrit. Aucune place ne peut être occupée deux fois. Exactement n−1 places restent libres. Elles reviennent aux cases du bord sans partenaire, pour lesquelles n'importe quelle place convient.

L'astuce décisive, ce sont les blocs. Des paires de même écart g peuvent s'empiler sans lacune. Pour g = 3, les paires (1, 4), (2, 5) et (3, 6) remplissent les places 1 à 6 sans trou. En général, g paires d'écart g remplissent exactement 2g places consécutives, puis vient le bloc suivant. Chaque groupe d'écart ne gaspille ainsi qu'au plus g−1 places à la fin de son dernier bloc. Les groupes d'écarts 1 à 12 coûtent ensemble au plus 0+1+…+11 = 66 places.

Le banc est divisé d'avant en arrière en cinq zones. Dans la première zone s'assoit la diagonale. Suit la fenêtre en étoile, où une rangée particulière de paires est imbriquée comme des arcs-en-ciel et où des paires d'écarts 6 et 8 s'insèrent dans les creux. Dans la fenêtre des forêts siègent des paires aux très grands écarts ; leurs partenaires se retrouvent loin derrière, dans une zone réservée. Viennent ensuite les classes résiduelles, c'est-à-dire toutes les autres paires d'écarts 1 à 12, en blocs. Enfin, les n−1 cases du bord prennent les places restantes.

Pourquoi le plan ne s'applique-t-il qu'à partir de n = 119 ? Le banc est presque exactement plein. Seules peuvent rester libres autant de places qu'il y a de cases du bord sans partenaire, soit n−1. Le plan perd au plus 117 places : 18 dans la fenêtre en étoile, 66 dans les blocs, 21 dans la fenêtre des forêts et 12 lors des sauts. Il fonctionne donc dès que n−1 vaut au moins 118. Pour n = 119, 118 places sont libres et au plus 117 sont perdues, il reste donc une place de réserve.

Pour les tailles plus petites, un programme informatique a cherché des plans de table adaptés et les a enregistrés sous forme de listes de nombres. Ces listes s'appellent des certificats. Lean revérifie lui-même chaque certificat au lieu de se fier au programme de recherche.

Pourquoi se fier à la preuve : Lean vérifie chaque étape

La preuve n'est pas seulement écrite, elle est contrôlée ligne par ligne par un vérificateur de preuves. Lean est un langage de programmation pour les preuves mathématiques. Chaque inférence y est notée si précisément que l'ordinateur peut la recalculer. Il n'y a ni lacunes ni « évidemment ». Une erreur ferait échouer la compilation.

On utilise pour cela Mathlib, la grande bibliothèque commune de mathématiques déjà vérifiées pour Lean, par exemple pour les règles de calcul sur les ensembles finis et les sommes. Dans la preuve finale, il n'y a pas un seul « sorry ». C'est le nom, en Lean, du marqueur qui permet de sauter provisoirement une étape. Il n'y a pas non plus d'axiome propre (une hypothèse de départ non démontrée) ni de confiance dans du code de programme compilé. À la fin, Lean peut lister les hypothèses sur lesquelles repose un théorème. Ici, il n'y a que les trois habituelles, sur lesquelles repose pratiquement toute Mathlib : propext, Classical.choice et Quot.sound.

Les programmes Python qui ont trouvé les certificats et le plan de construction n'ont pas besoin d'être sans faute. Un certificat erroné ou un plan de construction erroné serait rejeté par Lean. C'est le véritable gain de l'usage de l'IA et des programmes de recherche : les outils peuvent deviner, la vérification reste pourtant stricte.

Ce qu'un humain doit vérifier : la définition en cinq lignes

Une limite vaut pour toute preuve vérifiée par ordinateur : la définition du départ n'est pas vérifiée, elle est supposée. Dans le cas présent, la définition ne fait que cinq lignes, et elle dit en langage courant ceci : il existe un remplissage des cases avec des nombres entiers. Deux cases ne portent jamais la même valeur. Les valeurs utilisées sont exactement les nombres de −K à K. Chaque rangée, dans chacune des trois directions, a pour somme 0. Dans la version renforcée, le 0 se trouve en outre au centre.

Trois échappatoires possibles sont exclues. Premièrement, cases et nombres correspondent : l'hexagone compte 3n(n−1)+1 cases, et de −K à K il y a exactement autant de nombres, « chaque nombre exactement une fois » est donc imposé. Deuxièmement, les valeurs hors du nid d'abeilles ne comptent pas, toutes les conditions ne portent que sur des cases de l'hexagone. Troisièmement, les rangées hors du nid d'abeilles sont vides, leur somme vaut automatiquement 0, ce qui est inoffensif. La formule de K utilise la division entière, ce qui est sans danger, car n(n−1) est toujours pair.

Lors du contrôle, une lacune a en outre été repérée, depuis comblée. La définition d'origine n'exigeait pas expressément le 0 au centre. La construction le fournit certes toujours, car des cases symétriques portent des valeurs opposées. Il existe néanmoins désormais la définition renforcée avec la condition supplémentaire que le centre vaut 0, et le second théorème principal la prouve pour tout n à partir de 3.

Une part de confiance subsiste, comme pour toute preuve formelle. Elle concerne le petit noyau de vérification de Lean et les définitions de base de Mathlib, par exemple pour les sommes et les intervalles. Une préversion de Lean 4 a été utilisée. De plus, la vérification n'a eu lieu jusqu'ici que dans un seul environnement. On sera plus sûr si quelqu'un compile les fichiers de façon indépendante sur sa propre machine. En option, un programme de contrôle séparé comme lean4checker peut revérifier les fichiers de preuve terminés. Pour les petites tailles, on peut en outre afficher un hexagone concret et le recalculer à la main. Cela ne prouve rien de plus, mais montre de façon parlante que la définition correspond à l'intention.

Chiffres et faits sur la preuve

Sur l'énoncé : un hexagone magique de somme nulle est prouvé pour tout ordre n à partir de 3, y compris avec le 0 au centre. Des hexagones tout faits existent pour n = 3 à 6. Pour n = 7 à 118, des certificats fournissent la solution de l'énigme des bases, dont 57 sont nouveaux, à savoir ceux pour n = 62 à 118. Le plan de construction général s'applique à partir de n = 119, soit le rayon 118. Il perd au plus 117 places et laisse au moins une place de réserve pour n = 119. Le plus grand ordre de certificat est n = 118, ce qui correspond à 6 903 cases dans le triangle.

Sur l'ampleur : les étapes 1 à 4 et les certificats jusqu'à n = 61 sont réunis dans un fichier de 2 713 lignes. L'étape 5 se compose de 40 fichiers d'environ 7 000 lignes. Le besoin en mémoire le plus élevé est de 5,9 gigaoctets, pour un fichier consacré à la première ligne du plan de construction. On a utilisé Lean 4 dans la préversion v4.35.0-rc4 et Mathlib. Seuls propext, Classical.choice et Quot.sound apparaissent comme axiomes, il n'y a aucune lacune ouverte.

Sur le temps de calcul : la reconstruction de l'étape 5 dure environ 38 minutes, les certificats demandent environ 23 minutes en parallèle. Certains fichiers prennent nettement plus de temps. Le fichier des étapes 1 à 4 demande 460 secondes, le fichier auxiliaire des formules d'écarts souhaités 897 secondes, les certificats pour n = 62 à 89 encore 437 secondes et ceux pour n = 90 à 117 encore 927 secondes. Les fichiers de la première ligne demandent ensemble environ 18 minutes. Ces durées décrivent la reconstruction de la vérification finale. L'ensemble de la démonstration automatisée, avec recherche et développement, a coûté quelques heures.

Sur les tests préalables : le plan de construction a été testé numériquement avant la preuve Lean, comme reproduction exacte des définitions pour les rayons 118 à 450. Les énoncés auxiliaires ont été vérifiés jusqu'au rayon 20 000. Ces tests n'étaient qu'une vérification préalable, la preuve elle-même est le texte Lean.

La suite : questions ouvertes et mise en perspective

Le travail de Gukov et la preuve Lean se complètent. Gukov a fourni le motif, la construction et une esquisse avec la limite 114. L'esquisse n'a pas recalculé les lacunes de la première ligne et des forêts. Placées naïvement, il aurait manqué là ensemble environ 2n à 3n places, plus que les n−1 autorisées. La preuve Lean s'attaque précisément à ce point. Elle fournit des formules pour les écarts souhaités, un plan d'empaquetage avec au plus 117 places perdues au lieu de 2n à 3n, et de nouveaux certificats pour les ordres 62 à 118. Tous les ordres à partir de 3 sont ainsi couverts.

Reste d'abord le contrôle indépendant : une reconstruction sur une machine tierce (déjà réalisée par l'auteur), si possible avec lean4checker, et une relecture par des spécialistes. Les fichiers Lean ne sont pas encore liés publiquement dans cette description. Gukov pose en outre sur son site une question à laquelle la preuve ne répond pas : pourquoi les valeurs des cases semblent-elles aléatoires alors que les champs de potentiel correspondants paraissent lisses ? D'autres variantes de l'énigme sont envisageables, rien n'est promis à ce sujet.

Une énigme qui a commencé avec une figure en nid d'abeilles de 19 cases est résolue pour toutes les tailles. Il a fallu d'abord l'idée d'un humain, puis l'IA comme chercheuse et assistante de preuve, et enfin un vérificateur qui ne croit aucun des participants, mais recalcule chaque étape.