💻 computer science

SATisfying the High School Identities but not Wilkie's Identity

Cet article résout une question ouverte du problème de l'algèbre du lycée de Tarski en prouvant qu'aucune algèbre à 11 éléments ne peut satisfaire les identités de l'algèbre du lycée tout en réfutant l'identité de Wilkie, un résultat établi via un encodage SAT et accompagné de la découverte d'un nouveau contre-modèle à 12 éléments.

Auteurs originaux : Agon Hajdari, Johannes Niederhauser

Publié 2026-08-18

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Agon Hajdari, Johannes Niederhauser

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

Dans le vaste paysage des mathématiques, il existe un coin tranquille dédié aux règles qui régissent la manière dont nous combinons les nombres. Depuis des siècles, les mathématiciens s'appuient sur un ensemble standard de règles pour l'addition, la multiplication et l'élévation des nombres à des puissances — des opérations si fondamentales qu'elles sont enseignées au lycée. Ces règles semblent absolues, comme les lois de la physique, car elles fonctionnent parfaitement lorsque nous comptons des pommes ou calculons des distances. Cependant, une question profonde a persisté dans l'esprit des logiciens : ces règles familières du lycée sont-elles suffisantes pour expliquer chaque vérité sur ces opérations ? Pourrait-il exister une règle cachée, vraie pour tous les nombres naturels, qui ne puisse être dérivée des identités standards des manuels scolaires ? Cette question, connue sous le nom de problème de l'algèbre du lycée de Tarski, a remis en question la complétude de notre fondement mathématique. Si une telle règle cachée existait, cela signifierait que notre ensemble standard d'axiomes serait incomplet, laissant une lacune dans notre compréhension de l'arithmétique.

Pendant des décennies, la réponse est restée insaisissable. Dans les années 1980, un mathématicien nommé Alex Wilkie a découvert une règle spécifique et complexe qui est vraie pour les nombres naturels mais qui ne peut être prouvée en utilisant uniquement les identités standards du lycée. Ce fut une percée, mais cela laissa un nouveau puzzle : quelle peut être la taille minimale d'un « contre-exemple » ? Un contre-exemple, dans ce contexte, est un monde mathématique imaginaire où les règles standards sont respectées, mais où la règle spécifique de Wilkie échoue. Trouver un tel monde prouve que les règles standards ne sont pas suffisantes. Les chercheurs ont passé des années à chercher la version la plus petite possible de ce monde. En 2005, ils avaient construit un contre-exemple comprenant douze éléments distincts, et ils avaient rigoureusement prouvé qu'aucun contre-exemple ne pouvait exister avec dix éléments ou moins. Cela laissait un seul écart obstiné : un contre-exemple pourrait-il exister avec exactement onze éléments ?

Une équipe de chercheurs de l'Université d'Innsbruck a enfin comblé cet écart. Ils ont abordé le problème non pas en essayant de construire le monde mathématique à la main, mais en traduisant toute la recherche en un immense casse-tête logique qu'un ordinateur pourrait résoudre. Ils ont pris les exigences pour un monde mathématique valide — où l'addition et la multiplication se comportent normalement — ainsi que la condition spécifique que la règle de Wilkie doit échouer. Ils ont ensuite demandé à un ordinateur de vérifier chaque façon possible d'organiser un monde de onze éléments pour voir si l'une d'entre elles satisfaisait les conditions. L'ordinateur, utilisant des techniques avancées pour décomposer le problème en des milliards de minuscules étapes logiques, a trouvé qu'aucune de ces configurations n'existait. La recherche était exhaustive et les résultats ont été vérifiés indépendamment par différents outils logiciels pour garantir une certitude absolue. La conclusion est définitive : il n'existe pas de contre-exemple avec onze éléments. Le plus petit contre-exemple possible doit comporter au moins douze éléments.

Les chercheurs ne se sont pas arrêtés à la preuve du négatif. Dans le processus de leur recherche, ils ont également examiné le cas des douze éléments, qui était déjà connu comme étant possible. Ils ont découvert un nouveau monde de douze éléments, distinct, qui n'avait jamais été vu auparavant. Ce nouveau monde se comporte différemment de celui trouvé en 2005, prouvant qu'il existe plus d'une façon de briser les règles de l'algèbre du lycée tout en maintenant le reste du système intact. Pour parvenir à ces conclusions, l'équipe a utilisé de puissantes ressources de calcul parallèle, faisant tourner la recherche sur des dizaines de processeurs simultanément. Ils ont généré une preuve numérique pour leurs résultats, un certificat que d'autres mathématiciens peuvent vérifier pour s'assurer que l'ordinateur n'a pas commis d'erreur. Ce processus de vérification a confirmé que la recherche d'un contre-exemple de onze éléments était véritablement complète et que la réponse est un « non » catégorique.

Ce travail résout une question ouverte de longue date dans le domaine de la logique équationnelle, confirmant que le nombre douze est le seuil critique où ces anomalies mathématiques apparaissent pour la première fois. Il démontre que les identités standards du lycée sont suffisantes pour décrire toutes les vérités arithmétiques pour tout système de moins de douze éléments. L'étude souligne également le pouvoir croissant de l'informatique moderne pour résoudre des problèmes théoriques profonds. Ce qui était autrefois une tâche nécessitant des années d'effort manuel et d'intuition humaine ingénieuse a été transformé en un processus de vérification rigoureux et automatisé. Les chercheurs ont fourni à la communauté mathématique une carte complète du paysage jusqu'à la taille douze, montant exactement où les règles connues tiennent et où elles se brisent enfin. Leurs découvertes ne sont pas seulement une liste de nombres, mais une ligne de démarcation définitive dans notre compréhension de la structure arithmétique, tracée avec la précision d'une preuve vérifiée par ordinateur.

Résumé Technique : Satisfaire les identités du lycée mais pas l'identité de Wilkie

Énoncé du problème
Le document traite d'un cas spécifique du problème des identités du lycée de Tarski, qui demande si toute identité impliquant l'addition, la multiplication et l'exponentiation qui est vraie sur les entiers naturels ( $\mathbb{N}$ ) est dérivable des Identités du Lycée (HSI - High School Identities). Wilkie a précédemment démontré que ce n'est pas le cas en présentant une identité vraie dans $\mathbb{N}$ mais non dérivable des HSI. Pour prouver la non-dérivabilité, il faut construire un modèle fini (un contre-modèle) qui satisfait toutes les axiomes des HSI mais qui falsifie l'identité de Wilkie.

Avant ce travail, la recherche du plus petit contre-modèle de ce type s'était resserrée sur un cas unique : alors qu'un contre-modèle à 12 éléments était connu, des recherches exhaustives avaient exclu les tailles allant jusqu'à 10, laissant l'existence d'un contre-modèle à 11 éléments comme la dernière question ouverte.

Méthodologie
Les auteurs formulent la recherche de contre-modèles finis comme un problème de satisfiabilité propositionnelle (SAT). Leur approche implique :

Contraintes algébriques et élagage : Les auteurs intègrent des contraintes structurelles dérivées de la littérature algébrique antérieure (Burris, Lee, Zhang) pour réduire l'espace de recherche. Celles-ci incluent :
- La fixation de la chaîne « entière » ( $1, 1+1, 1+1+1$ ) à des éléments distincts $1, 2, 3$.
- La fixation de la paire de témoins $(a, b)$ qui falsifie l'identité de Wilkie à des éléments non entiers spécifiques $4$ et $5$.
- L'imposition de conditions d'« effondrement d'entiers » (inégalités) pour empêcher le modèle de dégénérer en une structure où l'identité de Wilkie serait accidentellement vraie.
- L'imposition de lemmes de divisibilité pour garantir que les termes spécifiques de l'identité de Wilkie ne satisfont pas de relations qui forceraient l'identité à être vraie.
Encodage SAT : Le problème est encodé en Forme Normale Conjonctive (CNF).
- Variables : Des variables booléennes représentent les tables d'opérations pour $+$ , $\times$ , et $\exp$ sur un domaine de taille $n$ . Des variables supplémentaires suivent l'évaluation des termes composites au sein de l'identité de Wilkie.
- Clauses : L'encodage impose que les opérations soient des fonctions totales (exactement une sortie par paire d'entrées), satisfont tous les axiomes HSI (associativité, commutativité, distributivité, lois de l'exponentiation, lois de l'identité), et encode explicitement la négation de l'identité de Wilkie ( $LHS \neq RHS$ ).
- Complexité : Le nombre de variables croît en $\Theta(n^3)$ , tandis que le nombre de clauses croît en $\Theta(n^7)$ . Pour $n=11$ , l'instance contient environ 3 069 variables et 63,8 millions de clauses.
Résolution et Vérification : Les auteurs utilisent des solveurs SAT parallèles (Gimsatul et MallobSat) pour résoudre les instances générées. Crucialement, ils utilisent des solveurs produisant des certificats pour générer des certificats d'insatisfiabilité (formats DRAT et LRUP). Ces preuves sont vérifiées indépendamment à l'aide de vérificateurs formellement vérifiés (GRAT et lrat_isa) afin de garantir que les résultats sont mathématiquement rigoureux et exempts d'erreurs d'implémentation de solveur.

Contributions clés et Résultats

Résolution du cas $n=11$ : Le résultat principal est la preuve qu'aucune algèbre à 11 éléments ne satisfait les axiomes HSI tout en réfutant l'identité de Wilkie. En montrant que toutes les instances SAT pour $n \le 11$ sont insatisfiables, les auteurs tranchent la dernière taille ouverte en dessous de 12.
Vérification : Les résultats d'insatisfiabilité sont appuyés par des certificats vérifiés de manière indépendante, offrant un haut degré de confiance dans la conclusion.
Nouveau contre-modèle à 12 éléments : Comme sous-produit du test de l'encodage pour $n=12$ , les auteurs ont découvert un contre-modèle à 12 éléments qui n'est pas isomorphe à l'exemple connu précédemment. Ils ont également identifié qu'il existe plus de 500 algèbres de Gurevič–Burris (GBA) non isomorphes à 12 éléments, bien qu'une énumération complète n'ait pas été réalisable dans leur temps imparti.
Analyse de performance : L'étude démontre que les solveurs SAT parallèles modernes sont capables de gérer la haute complexité équationnelle de ce problème, une tâche qui était auparavant considérée comme trop difficile pour les approches basées sur le SAT (comme le note le travail de Zhang en 2005). MallobSat s'est avéré nettement plus rapide que Gimsatul et la base mono-thread (CaDiCaL) pour les instances plus grandes ( $n \ge 10$ ).

Signification
L'article prétend régler la dernière taille ouverte pour la recherche de contre-modèles finis de l'identité de Wilkie, confirmant que 12 est la plus petite taille à laquelle de tels contre-modèles peuvent apparaître. Ce travail sert de démonstration des progrès du raisonnement automatisé, montrant que les solveurs SAT modernes peuvent efficacement traiter des problèmes de logique équationnelle complexes qui étaient auparavant intraitables pour ces outils. Les auteurs soulignent que leur contribution est la résolution définitive du cas $n=11$ par une résolution SAT rigoureuse et vérifiée par machine, plutôt que la découverte d'une nouvelle théorie algébrique ou d'applications dépassant le cadre du problème de Tarski.

Articles similaires