Travaux · Épreuves externes
Treize problèmes que nous ne corrigeons pas nous-mêmes
Un moteur qui se mesure à ses propres critères finit toujours par avoir raison. Nous avons donc pris treize problèmes ouverts ou compétitifs dont le barème appartient à quelqu’un d’autre : tables publiques, vérificateurs officiels, arbitres nommés. Cette page dit ce qui est passé, ce qui a échoué, et ce que nous avons dû retirer.
Pourquoi des épreuves externes
Le reste de ce site repose sur des protocoles que nous écrivons, des empreintes que nous calculons, des gates que nous définissons. C’est vérifiable, mais c’est auto-mesuré.
Un problème ouvert de la littérature ne se négocie pas. La table de Packomania est tenue par Eckard Specht ; les cases vides de l’OEIS sont vides pour tout le monde ; le vérificateur d’un board renvoie un code de sortie qui ne tient aucun compte de nos intentions. C’est le seul régime où se tromper coûte quelque chose.
Chaque challenge suit la même procédure : revue de la littérature avant d’écrire une ligne de code, préenregistrement scellé de ce qu’on cherche et de ce qui comptera comme succès, puis certification mécanique. Un challenge ne démarre pas sans sa revue de littérature — le lanceur refuse.
La carte des treize
| Nº | Sujet | État |
|---|---|---|
| 001 | Fractions égyptiennes 5/n (Erdős–Straus) | théorèmes de couverture prouvés algébriquement · 1 claim retiré |
| 002 | Exceptions de Schinzel 20/n | 72 exceptions, aucune nouveauté — validation du moteur |
| 003 | Extension Pomerance–Weingartner | 30 listes certifiées · brouillons OEIS prêts |
| 004 | IBM Ponder This, septembre 2026 | 45 termes — égale la référence, pas un record |
| 005 | Packomania — cercles à rayons libres | 60 records candidats + 155 premières entrées |
| 006 | Triangles de Kobon | 8 premières bornes pour des cases vides de l’OEIS |
| 007 | Multiplication matricielle rapide | Strassen certifié par le noyau Lean, sans axiome |
| 008 | Carrés dans un carré | outil déclaré inapte — aucune tentative |
| 009 | Nombre chromatique du plan | deux lemmes de de Grey et le graphe de Parts vérifiés |
| 010 | Complexité entière de 2⁶¹−1 | 133 uns contre une base de 150, vérificateur officiel |
| 011 | Distances unité rationnelles | 119 bornes inférieures revalidées par le scoreur officiel |
| 012 | ESA SpOC — Programmable Cubes | en cours |
| 013 | Asymptotique de Σr | en cours |
Packomania — 60 candidats certifiés
Le problème : placer N cercles de rayons libres dans un carré unité en maximisant la somme des rayons. La table de référence est publique et tenue depuis des années ; ses détenteurs sont nommés — Specht, Tariq, Cantrell, Castro, Sander.
Au 16 septembre 2026, le dossier compte 60 records candidats et 155 premières entrées — des cases que la table laissait vides. Soit 215 fichiers, audit exact contre la table du jour, 0 problème, et 60 certificats Lean vérifiés sans aucun axiome.
Le dossier de soumission est constitué pour être rejoué par un tiers : vérificateurs adaptés pour tourner depuis le dossier, table de référence du jour, journaux, manifeste SHA-256. Les limites y sont écrites noir sur blanc — aucune optimalité prouvée, premières entrées améliorables, marges exposées sur quatre cases.
Le mot candidat est littéral : la table bouge. Le 16 septembre au matin, la case N = 119 nous a été reprise par un tiers ; elle a été retirée du dossier, puis regagnée le soir même. Une case publiée par Castro au-dessus de notre valeur nous a fait retirer notre entrée. Un record sur une table vivante n’est pas un acquis, c’est une position.
Kobon — huit cases vides remplies
Combien de triangles peut-on former avec k droites dans le plan ? Le problème est ouvert ; l’OEIS en tient la table, avec des cases vides.
Huit de ces cases ont reçu une première borne inférieure : k = 35, 36, 39, 40, 43, 44, 47, 48.
Et un résultat d’un autre genre : l’auteur d’un jeu de données publié — les quinze arrangements optimaux à k = 14 de Maiorana — demandait une confirmation indépendante. Nos deux compteurs, écrits séparément, trouvent 54 triangles chacun sur les quinze. Confirmer le travail d’un autre ne rapporte aucun record ; c’est pourtant ce que la littérature réclamait.
Plan chromatique — vérifier avant de prétendre
Combien de couleurs faut-il pour colorier le plan de sorte que deux points à distance 1 diffèrent ? La question est ouverte depuis 1950. En 2018, Aubrey de Grey a montré qu’il en faut au moins 5 ; le plus petit graphe connu qui l’établit compte aujourd’hui 509 sommets, dû à Jaan Parts.
Nous n’avons pas battu ce record. Nous avons fait autre chose :
- Les deux lemmes clés de de Grey ont été revérifiés indépendamment, avec certificat mécanique : négation encodée en clauses, réfutation par solveur, puis preuve relue par un vérificateur tiers. La plus grosse fait 6,32 Mo et 2,6 millions d’étapes de résolution.
- Le graphe de Parts a été relu exactement — et le contrôle a refusé deux fois nos hypothèses avant de passer : le graphe n’habite pas le corps que nous supposions, et l’une de ses coordonnées contient un radical imbriqué.
- Ses 509 sommets sont tous nécessaires : 509 témoins de criticité validés sans solveur, 0 défaut. Conséquence directe — battre 509 exige des sommets nouveaux, aucun sous-graphe ne suffira.
Notre meilleur graphe 5-chromatique distinct compte 515 sommets. C’est six de trop. Nous l’écrivons parce que c’est le résultat.
Ce qui n’est pas un record, et qu’on le dise
- IBM Ponder This — 45 termes. Cette progression arithmétique égale la longueur affichée par la référence (B. Felgenhauer). Elle ne la dépasse pas. Une recherche exhaustive de 46 termes est revenue négative sous 10¹³.
- Exceptions 20/n — 72 trouvées. Elles retrouvent un fait numérique déjà publié par Pomerance et Weingartner. Aucune nouveauté mathématique : c’est le moteur qui est validé, pas la mathématique qui avance.
- Plan chromatique — 515 sommets. Dix sommets au-dessus du record, et des valeurs intermédiaires meilleures sont déjà publiées. Ce n’est pas un record et n’en approche pas un.
Ce que nous avons retiré
Cinq affirmations ont été annulées après avoir été écrites. Elles figurent ici parce qu’un registre qui ne contient que des succès n’est pas un registre.
| Affirmation | Pourquoi elle est tombée |
|---|---|
| Kobon : « UNSAT ⇒ a(18) = 93 » | hypothèse de modélisation cachée — l’encodage ne couvrait que les arrangements simples, alors que l’optimum à k = 8 utilise des points triples |
| IBM : « mur à 41 termes » | artefact de couverture — trois pas testés sur environ quatre-vingts, pris pour une impossibilité |
| Plan chromatique : « une seule classe de translation est bonne » | artefact d’échantillonnage — quatre classes sur vingt-quatre observées ; le balayage complet en donne quatorze |
| 5/n : une généralisation | sur-généralisation avant vérification — leçon fondatrice du vocabulaire fermé |
| Packomania : valeur prédictive d’un outil de ciblage | validation en partie circulaire, détectée à l’audit |
Le challenge le plus instructif est un échec
Sur « carrés dans un carré », l’étalonnage a donné 0 sur 2 : l’outil n’a pas retrouvé deux configurations connues. Il a été déclaré inapte et aucune tentative n’a été faite sur le cas ouvert.
Une fausse amélioration avait été fabriquée pendant la mise au point, puis écartée par le contrôle. C’est précisément ce qu’un étalonnage sert à attraper — et c’est pourquoi on ne le saute pas.
Portée du résultat
- Aucune soumission n’a été envoyée. Les brouillons destinés à Specht, à IBM, à Maiorana et aux boards sont prêts ; les envoyer est un geste qui appartient au porteur, pas au moteur.
- Les records Packomania sont des candidats : aucune optimalité n’est prouvée, et la table de référence change sous nos pieds.
- Les bornes de Kobon et les tables de distances unité sont des bornes inférieures. Elles ne prouvent aucune optimalité.
- Sur le plan chromatique, rien n’est revendiqué comme nouveau : deux lemmes publiés ont été revérifiés, un graphe publié a été relu. La valeur est dans la chaîne de vérification, pas dans le résultat.
- L’apport propre de chaque composant du moteur n’est pas établi — une étude d’ablation est proposée, pas faite.
- Aucune cognition n’est établie. Le dispositif est un pipeline qui engendre, réfute et vérifie ; il n’invente pas de preuves d’énoncés nommés.
Sources publiques employées sous leur licence : données de Maiorana (CC BY 4.0), outils de vérification de preuves sous licence MIT, coordonnées de Parts inchangées. Un jeu de données sans licence explicite a été écarté de tout usage, ses résultats publiés restant seulement citables.