Contexte et objectif
Le problème du packing de carrés consiste à placer un nombre donné de carrés dans un carré plus grand sans chevauchement et en minimisant la longueur du côté du contenant. Pour 11 carrés, la valeur optimale était connue uniquement sous forme conjecturale. Le dépôt 11SquaresFormalized propose une preuve complète, vérifiée dans le système de preuve assistée par ordinateur Lean, afin de rendre la démonstration irréfutable du point de vue formel.
Méthodologie de formalisation
Les auteurs ont structuré la démonstration en 7 920 modules Lean, chacun compilé avec la version 4.34.1 du noyau et la révision d4c23b du mathlib. Les parties géométriques sont exprimées avec des certificats numériques exacts, évalués par la primitive native_decide. Cette approche combine des preuves classiques (raisonnement par cas, couverture de cellules fermées) avec des calculs numériques certifiés, garantissant que le noyau Lean et le compilateur natif sont les seules sources de confiance. Le processus d’audit final exige zéro admission d’axiome et le drapeau OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES, ce qui exclut toute vérification « kernel‑only ».
optimal_side_length T = (6*u + 4) / (1 + 2*u - u^2)
where u solves 5*u^8 - 10*u^7 - 2*u^6 + 14*u^5 + 12*u^4 - 6*u^3 + 2*u^2 + 2*u - 1 = 0
Résultats numériques et vérification
Le polynôme d’ordre huit possède une racine unique u dans l’intervalle (9/25, 37/100). En substituant cette racine, le côté optimal du carré contenant vaut approximativement 3.8770835900228141773. La construction associée atteint exactement cette longueur, ce qui prouve qu’aucune configuration ne peut être plus compacte. Tous les certificats numériques sont consignés dans verification/native-certificates.json avec leurs hachages source, assurant la traçabilité complète. La compilation séquentielle des modules, bien que longue (2–3 h sur macOS), aboutit à 100 % de modules compilés, condition indispensable mais non suffisante pour la validation finale.
Limites et perspectives
La preuve repose sur le modèle de confiance « lean_kernel_and_native_compiler », ce qui implique que toute faille du compilateur natif pourrait affecter la validité. Le dépôt ne fournit pas de comparaison de performances entre cette approche et des méthodes purement algorithmiques (par exemple, recherche exhaustive ou optimisation linéaire). De plus, la formalisation reste spécifique à la configuration de 11 carrés ; l’extension à d’autres nombres ou à des contraintes supplémentaires (orientations fixes, bordures strictes) nécessiterait une refonte substantielle du cadre de preuve. Néanmoins, le travail démontre la faisabilité d’associer calcul exact et preuve formelle pour un problème géométrique non trivial, ouvrant la voie à des vérifications similaires dans la combinatoire et la géométrie discrète.
