Expérience · Géométrie

Packomania : des empilements de cercles exacts et certifiés

Cette expérience porte sur un problème de géométrie classique : placer N cercles de rayons libres dans un carré, sans chevauchement, pour que la somme des rayons soit la plus grande possible. L’arbitre est la table « csqv » de Packomania. Résultat : 367 des 583 entrées de la table sont issues de l’expérience. Chaque empilement est exact, accompagné d’un certificat que n’importe qui revérifie, et se revérifie à l’identique. Une borne démontrée sert de règle : les entrées de l’expérience atteignent de 92,7 % à 94,3 % de cette borne.

1. La question

Pour chaque nombre N de cercles, quelle somme maximale de rayons peut-on atteindre dans un carré unité ? Les rayons sont libres : chaque cercle choisit sa taille. Aucune formule ne donne la réponse ; la table recense 583 entrées (N de 1 à 500 sauf N = 493, et 84 valeurs plus grandes jusqu’à N = 10 000), chacune avec la meilleure valeur connue et l’empilement qui la réalise. La question de l’expérience : établir des empilements exacts et vérifiables pour un grand nombre d’entrées.

2. Protocole de vérification

Chaque résultat est un fichier de N lignes (x, y, r), soumis à l’arbitre, qui le publie dans sa table, et contrôlé par un vérificateur exact indépendant du programme qui a produit la solution (section 5). Les chiffres de cette page sont ceux de la table relevée à la date indiquée.

L’arbitre et son site

Packomania est le site où Eckard Specht tient les tables des meilleurs empilements connus ; la table « csqv » concerne les cercles de rayons libres dans un carré. Elle repose sur son programme csqv (« 2011–2026 », page des références de la table) et sur les contributions de chercheurs : chaque entrée porte la référence de son auteur, et les actualités de la page consignent chaque mise à jour avec sa date. Le 04/10/2026, il y note : « graphs with normed mean radius R(N) = sum_of_radii / N^1/2 versus N can be plotted, which show a nearly constant function. But there are slight periodic oszillations » (sic ; packomania.com/csqv/csqv.html, actualités du 04/10/2026).

3. Résultats de la table

Les trois graphiques suivants sont tracés à partir des valeurs de la table du 30/09/2026 pour N ≤ 500 (499 entrées). Les points cyan marquent les entrées issues de l’expérience, les cercles blancs les empilements présentés plus bas, le cercle or N = 69.

Trois empilements, tracés à partir des coordonnées exactes de l’entrée déposée : le centre et le rayon de chaque cercle. La couleur suit le rayon, du violet (petit) au cyan (grand). Les cercles apparaissent de gauche à droite : c’est un balayage d’affichage, sans lien avec le calcul. Les données de chaque figure sont téléchargeables en JSON.

4. Une borne et le rapport de chaque entrée

La table classe les entrées entre elles. Une borne supérieure démontrée donne une règle fixe : aucun empilement de N cercles disjoints dans le carré unité ne peut dépasser √(N/π) pour la somme des rayons. Le rapport de chaque entrée à cette borne se lit à la date de la table.

Théorème T1. Pour tout empilement de n cercles deux à deux disjoints contenus dans le carré unité, Σ r_i ≤ √(n/π).

Preuve. Les disques sont disjoints et contenus dans le carré d’aire 1, donc Σ π r_i² ≤ 1. Par Cauchy–Schwarz appliqué à (r₁, …, r_n) et (1, …, 1), (Σ r_i)² ≤ n · Σ r_i² ≤ n/π. ∎

Cette borne est élémentaire : elle tient en deux lignes (aire et Cauchy–Schwarz). Sa preuve est écrite ci-dessus ; elle n’est pas formalisée dans Lean. Elle sert ici de règle de mesure pour toute la table.

Le contrôle de la borne (distinct du certificat de validité d’un empilement) vérifie π·(Σ r)² ≤ n en arithmétique rationnelle exacte seule (aucun nombre flottant n’intervient dans la décision) : π est encadré par deux rationnels à 30 décimales, et c’est la borne supérieure de π qui sert au test. Le rapport à la borne est rendu sous forme d’encadrement rationnel ; aucune racine n’est extraite pour décider. Le 11/10/2026, appliqué aux 583 entrées de la table du 30/09/2026, il les déclare toutes conformes (somme publiée, 12 décimales). Les entrées de l’expérience atteignent de 92,7 % (N = 54) à 94,3 % (N = 426) de la borne ; l’ensemble de la table va de 73,4 % (N = 2) à 94,9 % (N = 10000). Sur les fichiers déposés, en rationnels exacts : N = 54, 92,7 % ; N = 69, 93,0 % ; N = 101, 93,3 % ; N = 200, 93,9 % ; N = 500, 94,3 %.

Ce rapport ne change pas quand une valeur de la table est battue.

La porte de réfutation

Un contrôle n’a de valeur que s’il rejette ce qui est faux. Le contrôle de la borne a été éprouvé sur un empilement de 300 cercles déposé le 24/09/2026 : la borne √(300/π) vaut 9,7720502380583984 ; il accepte la somme réelle (9,188348093925) et rejette une somme fabriquée juste au-dessus de la borne (9,7720502380584). Il discrimine, il ne se contente pas de tout accepter.

5. Le certificat de validité

Le certificat de validité est le contrôle exact des N lignes d’un fichier, mené par un vérificateur indépendant du programme qui a produit la solution. Il n’utilise ni racine carrée ni tolérance : les valeurs décimales sont lues comme des nombres rationnels, et toutes les comparaisons se font sur ces rationnels.

Énoncé de validité

Proposition. Soit (x_i, y_i, r_i), i = 1…N, des nombres rationnels, et le carré Q = [−½, ½]². Si

1. pour tout i : r_i > 0, x_i − r_i ≥ −½, x_i + r_i ≤ ½, y_i − r_i ≥ −½ et y_i + r_i ≤ ½ ;
2. pour tout i < j : (x_i − x_j)² + (y_i − y_j)² ≥ (r_i + r_j)² ;

alors (a) chaque disque fermé D_i de centre (x_i, y_i) et de rayon r_i est contenu dans Q ; (b) les intérieurs de deux disques distincts sont disjoints (deux disques se touchent au plus en un point) ; (c) la somme des rayons des N disques vaut exactement Σ r_i, un nombre rationnel calculé sans arrondi.

Démonstration

(a) Si (X, Y) appartient à D_i, alors |X − x_i| ≤ r_i, donc X ∈ [x_i − r_i, x_i + r_i] ⊂ [−½, ½] par la condition 1 ; de même pour Y.

(b) Si un point P était dans l’intérieur de D_i et de D_j, l’inégalité triangulaire donnerait |c_i − c_j| ≤ |c_i − P| + |P − c_j| < r_i + r_j, donc |c_i − c_j|² < (r_i + r_j)², ce qui contredit la condition 2.

(c) C’est une somme finie de rationnels.

Ce que le certificat garantit

• que les N cercles tiennent dans le carré, sans en sortir, même d’une quantité infime ;
• qu’aucun couple de cercles ne se chevauche : au plus, deux cercles se touchent ;
• la valeur exacte de la somme des rayons du fichier déposé ;
• que N cercles sont bien présents, ni plus ni moins.

Les théorèmes Lean déposés

Pour 62 certificats déposés, dont N = 54, les conditions de la proposition ci-dessus sont écrites comme théorèmes dans l’assistant de preuve Lean, instanciées sur cet empilement (fichiers CertN*.lean, sans bibliothèque externe). Les coordonnées y sont des entiers exacts, à l’échelle 10¹⁸. Rejeu du 11/10/2026 avec Lean 4.30.0-rc2 : chacun des 310 théorèmes est évalué par le noyau (decide +kernel) et Lean le déclare sans dépendance à un axiome (« does not depend on any axioms »). Ces théorèmes portent sur des empilements particuliers (nombre de cercles, inclusion, disjonction, somme, comparaison à la valeur antérieure), non sur la borne T1. Extrait pour N = 54 :

-- Extrait de CertN54.lean (N = 54, échelle S = 10^18, cercle = (x, y, r) en entiers, carré [0, S]²)
abbrev Inside (c : Int × Int × Int) : Prop :=
  0 < c.2.2 ∧ c.2.2 ≤ c.1 ∧ c.1 + c.2.2 ≤ S ∧ c.2.2 ≤ c.2.1 ∧ c.2.1 + c.2.2 ≤ S
abbrev Disj (c d : Int × Int × Int) : Prop :=
  (c.2.2 + d.2.2) * (c.2.2 + d.2.2) ≤
    (c.1 - d.1) * (c.1 - d.1) + (c.2.1 - d.2.1) * (c.2.1 - d.2.1)

theorem length_eq        : circles.length = 54                      := by decide +kernel
theorem all_inside       : ∀ c ∈ circles, Inside c                  := by decide +kernel
theorem pairwise_disjoint: circles.Pairwise Disj                    := by decide +kernel
theorem sum_eq           : sumR = 3842678286690508252               := by decide +kernel

Le cinquième théorème du même fichier compare la somme à la valeur publiée avant le dépôt (3,842635794975), voir section 8.

Revérifier soi-même

Télécharger le fichier JSON d'un des empilements, puis exécuter ce court programme Python (bibliothèque standard seule). Il lit les coordonnées en rationnels exacts, teste les conditions 1 et 2 pour toutes les paires (N(N − 1)/2 paires, soit 124 750 pour N = 500) et affiche le résultat.

import json
from fractions import Fraction as F

d = json.load(open("packomania_500.json"))
P = [tuple(F(v) for v in c) for c in d["circles"]]   # (x, y, r) en rationnels exacts
h = F(1, 2)
dedans = all(r > 0 and x - r >= -h and x + r <= h and y - r >= -h and y + r <= h for x, y, r in P)
disjoints = all((a[0]-b[0])**2 + (a[1]-b[1])**2 >= (a[2]+b[2])**2
                for i, a in enumerate(P) for b in P[i+1:])
print(len(P), dedans and disjoints, float(sum(r for _, _, r in P)))

Résultat attendu pour N = 500 : 500 True 11.90174407201714. Les fichiers JSON contiennent aussi l'empreinte sha256 du fichier déposé auprès de l'arbitre.

6. N = 69 : un axe de symétrie médian

Les empilements symétriques de la table ont en général pour axe une diagonale du carré. Le 20 septembre 2026, l'arbitre relève pour N = 69 un axe qui est la médiane entre deux côtés opposés : « The candidate for N=69 is the very first which doesn't has a diagonal as a symmetry axes, but the midline between two opposite sides of the square. Are there more? » (sic). N = 70, qui a le même type d'axe, a été trouvé ensuite par Wilfred Heap, référence [17].

La figure animée montre l'entrée N = 69, tracée d'après ses coordonnées : les 69 cercles apparaissent, puis l'axe vertical est dessiné. À 10⁻¹⁴ près (écart maximal mesuré : 1,2 × 10⁻¹⁴), chaque cercle à gauche de l'axe a son image à droite, de même rayon et à la même hauteur. Le schéma dessous compare un axe diagonal (ici N = 34) et le cas médian de N = 69.

7. La carte du défi

Les entrées de N = 1 à 500, rangées par lignes de 20 : le numéro N d'une case est le numéro de début de sa ligne plus sa colonne moins 1 (la case en pointillés, N = 493, n'a pas d'entrée). Les traits horizontaux séparent les tranches de 100, avec le décompte des entrées issues de l'expérience. En bas, les 84 entrées de N > 500 (jusqu'à N = 10 000), dans l'ordre. Table du 30/09/2026.

8. Une amélioration d'empilement

Le 16/09/2026, la table affichait pour N = 54 une somme des rayons de 3,842635794975 (valeur publiée sur la table, coordonnées arrondies à 12 décimales, non revérifiées en exact, auteur non identifié). L'entrée déposée, vérifiée en exact, a pour somme 3,842678286691, soit un gain de 4,25 × 10⁻⁵. L'animation passe de l'empilement affiché par la table (violet) à celui de l'expérience (cyan) : c'est une transition d'affichage entre deux états publiés.

Le résultat déposé est figé : son sha256 est publié, et chacun le revérifie à l'identique.

9. Ce que modélise cette question

Ce type de question modélise des problèmes de placement qui se posent dans la découpe et l'emballage, le placement d'antennes ou de capteurs, l'étude des matériaux granulaires et la conception de puces. La table csqv sert de référence commune pour comparer des empilements de cercles de rayons libres. Les empilements présentés ici sont exacts, certifiés et revérifiables par n'importe qui.

Mon projet d'IA au service de ma recherche

Ce défi n'est pas un but en soi : c'est un banc d'essai de ma recherche sur une IA embarquée certifiable. Mon projet d'IA, dont le fonctionnement reste confidentiel, me permet d'atteindre 367 des 583 entrées de la table « csqv » de Packomania, chaque empilement revérifié en arithmétique exacte. Le certificat et l'arbitre en font foi : ce n'est pas mon explication qu'il faut croire, c'est le résultat qui se revérifie. Il s'agit du meilleur résultat connu à la date indiquée, pas d'un optimum démontré.