💻 computer science

The set of primes is supernatural: a Lean formalization of the statement of the conjecture

Cet article présente une formalisation complète et vérifiée par machine en Lean 4 de la conjecture selon laquelle aucune fonction non constante construite à partir de l'identité, de constantes et d'un nombre fini d'opérations ponctuelles (addition, multiplication, exponentiation) n'associe chaque entier positif à un nombre premier, transformant ainsi la conjecture en une cible précise et vérifiable par le noyau pour les systèmes de raisonnement automatisé.

Auteurs originaux : A. Mayeux

Publié 2026-08-11

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : A. Mayeux

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

Imaginez une vaste bibliothèque infinie où chaque livre est un nombre. Dans cette bibliothèque, il existe un club très spécial et exclusif appelé les « Primes ». Ce sont des nombres qui ne peuvent pas être construits en multipliant des nombres plus petits ; ils sont les atomes indivisibles de l'arithmétique, comme 2, 3, 5 ou 7. Pendant des siècles, des mathématiciens ont essayé d'écrire une recette unique et simple — une machine faite d'outils mathématiques de base — qui pourrait recracher uniquement ces membres spéciaux du club. Ils voulaient une machine qui, quel que soit le nombre que vous lui donneriez, produirait toujours un nombre Premier.

Les outils autorisés dans cette recette sont les plus basiques que nous connaissions : additionner des nombres, multiplier des nombres et élever des nombres à des puissances (comme le carré ou le cube). Vous pouvez mélanger et assortir ces outils autant que vous le souhaitez, mais vous ne pouvez pas utiliser rien de sophistiqué comme la division ou les racines carrées. La grande question est la suivante : est-il possible de construire une machine en utilisant uniquement ces outils simples qui ne commet jamais d'erreur ? Pourrait une telle machine générer une liste infinie de nombres premiers, ou finira-t-elle par trébucher et produire un nombre qui n'est pas premier ? Ce n'est pas seulement un jeu ; cela touche au cœur même de la structure des nombres. Si une telle machine existait, cela signifierait que les nombres premiers suivent un modèle simple et prévisible. Si ce n'est pas le cas, cela signifie que les nombres premiers sont sauvages, chaotiques et « surnaturels » d'une manière qui défie les formules simples.

Ce document est une enquête policière numérique sur cette question précise. L'auteur, Arnaud Mayeux, a pris un article mathématique spécifique qui proposait une supposition audacieuse (une conjecture) et a traduit l'intégralité de celui-ci dans un langage informatique appelé Lean. Considérez Lean comme un arbitre super strict qui vérifie chaque étape d'une preuve mathématique pour s'assurer qu'elle est 100 % logiquement saine, sans aucune place pour l'erreur humaine ou les moments de type « je pense que cela fonctionne ». Le papier ne résout pas le mystère de savoir si la machine génératrice de nombres premiers existe ; il construit plutôt un modèle numérique parfait et incassable des règles du jeu.

La découverte principale de ce travail est que toute la théorie derrière la supposition de la « Machine à Primes » a été codée avec succès dans l'ordinateur. Chaque définition, chaque exemple et chaque tableau de nombres de l'article original vit désormais à l'intérieur de ce fichier numérique. L'auteur a vérifié 89 exemples différents de ces « fonctions naturelles » (le nom sophistiqué pour les machines construites à partir de l'addition, de la multiplication et des puissances). Pour chaque fonction, l'ordinateur a calculé les résultats et a confirmé qu'elles finissent toutes par échouer à produire un nombre premier. Par exemple, une fonction a parfaitement fonctionné pour les six premiers nombres, mais a échoué au septième. L'ordinateur a prouvé ces échecs avec une certitude absolue, en utilisant des certificats numériques avancés pour vérifier de grands nombres qui prendraient des années à un humain pour être vérifiés à la main.

Cependant, l'article est très clair sur ce qu'il n'a pas fait. Il n'a pas prouvé que la Machine à Primes est impossible. Il n'a pas trouvé la réponse ultime. La supposition centrale — qu'aucune machine de ce type n'existe — reste un problème ouvert, un « problème ouvert nommé » dans le code informatique, attendant qu'un humain ou une intelligence artificielle le prouve enfin. Le papier dit essentiellement : « Voici le livre de règles exact, et voici la preuve que chaque machine que nous avons testée jusqu'à présent échoue, mais le verdict final est toujours en suspens. »

L'auteur a également élargi légèrement le jeu. Il a demandé : « Et si nous ajoutions quelques outils supplémentaires, comme les factorielles (multiplier un nombre par tous les nombres inférieurs à lui) ou les flèches de Knuth (une façon d'écrire d'énormes puissances) ? » Il a construit une nouvelle classe de machines plus large avec ces outils supplémentaires et a énoncé une nouvelle version, encore plus difficile, de la supposition : même avec ces super-outils, on ne peut toujours pas construire une machine qui ne produit que des nombres premiers. Cette nouvelle supposition est également laissée ouverte, non prouvée, mais elle est maintenant écrite d'une manière qu'un ordinateur peut vérifier si quelqu'un finit par trouver la preuve.

En résumé, ce papier est un acte massif de traduction et de vérification. Il prend une idée mathématique complexe sur la nature chaotique des nombres premiers et l'enferme dans un coffre-fort numérique où chaque règle est vérifiée par une machine. Il confirme que pour chaque exemple spécifique testé, la « Machine à Primes » échoue, mais il laisse la question ultime de savoir si une telle machine est théoriquement possible comme un défi pour l'avenir. Les nombres premiers, semble-t-il, sont effectivement « surnaturels », résistant à toute formule simple avec laquelle nous essayons de les piéger.

Résumé Technique : L'ensemble des nombres premiers est surnaturel : Une formalisation en Lean de l'énoncé de la conjecture

Énoncé du problème
L'article traite de la formalisation de la « Conjecture des Nombres Premiers Surnaturels » proposée initialement dans [3]. La conjecture postule qu'aucune fonction non constante, construite à partir de la fonction identité et de constantes en utilisant un nombre fini d'additions, de multiplications et d'exponentiations ponctuelles, n'envoie tout entier positif vers un nombre premier. L'article vise à traduire cette conjecture et son cadre théorique environnant en une formalisation vérifiée par machine utilisant Lean 4 et la bibliothèque Mathlib. L'objectif est d'établir une cible précise, vérifiée par le noyau (kernel), pour la conjecture, permettant aux systèmes de raisonnement humains et automatisés de tenter une preuve.

Méthodologie
La formalisation est entièrement contenue dans un seul fichier Lean 4, SPCL.lean (environ 1200 lignes), qui dépend uniquement de Mathlib. La méthodologie consiste en une traduction directe et exhaustive de l'article source [3] dans Lean, garantissant que chaque définition, exemple, remarque, résultat numéroté et ligne de tableau expérimental possède un équivalent vérifié par machine.

Composants techniques clés :

Structures d'élévation : L'article axiomatise les compatibilités de l'addition, de la multiplication et de l'exponentiation en tant que « structure d'élévation » (un 4-uplet $(E, +, \times, \wedge)$ ). Cela est formalisé comme une classe de types (type class), et la catégorie de ces structures est construite avec des lois d'identité et de composition.
Fonctions naturelles : Deux codages équivalents de « fonctions naturelles » sont implémentés :
1. Construction par mots : Les fonctions sont générées par des mots finis sur l'alphabet $\{A_+, A_\times, A_\wedge\}$ appliqués à l'ensemble des fonctions identité et constantes.
2. Clôture inductive : Un prédicat inductif IsNatural est défini avec des constructeurs pour l'identité, les constantes et les trois opérations.
  L'équivalence entre ces deux définitions est formellement prouvée.
Formulation de la conjecture : La conjecture est énoncée comme une proposition nommée (Conjecture_2_1) de type Prop sans preuve. Elle est explicitement définie comme une hypothèse plutôt que comme un axiome ou un théorème rempli de sorry, garantissant que la formalisation n'introduit aucune nouvelle hypothèse.
Vérification expérimentale : L'article formalise 89 résultats expérimentaux de [3, §4]. Ceux-ci sont énoncés comme des théorèmes affirmant la primalité de valeurs de fonctions spécifiques jusqu'à un certain point et la composité de la première valeur non-première.
- Pour les petites valeurs, les preuves reposent sur norm_num (évaluation computationnelle).
- Pour les valeurs élevées (ex. $2^{2^6} + 93$ ), la formalisation utilise des certificats de primalité de Lucas. Ceux-ci sont vérifiés via un lemme lucasCert personnalisé qui vérifie les conditions $a^{p-1} \equiv 1 \pmod p$ et $a^{(p-1)/q} \not\equiv 1 \pmod p$ pour les facteurs premiers $q$ de $p-1$ , en utilisant la tactique reduce_mod_char de Mathlib.

Contributions clés

Formalisation exhaustive : L'article fournit une formalisation complète et « sans sorry » de l'intégralité de l'article [3]. Chaque définition, lemme, proposition et ligne de tableau est présent dans le code Lean.
Cible de conjecture précise : En énonçant la conjecture comme un Prop nommé et non prouvé, ce travail crée un objectif spécifique et vérifiable pour les systèmes de raisonnement automatisés. La structure de dépendance est transparente ; toute preuve de la conjecture ne reposerait que sur les définitions et axiomes formalisés de Lean/Mathlib.
Extension mathématique : La formalisation étend la théorie de [3, Remarque 3.4] en définissant une classe plus large de fonctions, IsNaturalKnuthFactorialSub. Cette classe inclut :
- La notation de flèche de Knuth (où le niveau de la flèche est lui-même une fonction de la classe).
- La fonction factorielle.
- La soustraction tronquée (sous la condition $g(n) < f(n)$ ).
  L'article prouve que la classe originale des fonctions naturelles s'insère dans cette classe étendue.
Vérification des cas prouvés : La formalisation inclut des preuves pour les cas où la conjecture est connue pour être vraie (ex. polynômes non constants, formes linéaires-exponentielles et la fonction de Fermat), en utilisant des résultats de théorie des nombres standards de Mathlib (ex. divisibilité polynomiale, petit théorème de Fermat).

Résultats

Cohérence formelle : Le fichier SPCL.lean compile en environ 30 secondes. Il repose uniquement sur les axiomes classiques standards de Lean (extensionalité propositionnelle, validité des quotients, choix) hérités de Mathlib.
Tables expérimentales : Les 89 lignes des tables expérimentales de [3] sont formalisées sous forme de théorèmes. Les preuves pour les affirmations de primalité de grandes valeurs sont vérifiées via des certificats de Lucas vérifiés par le noyau, éliminant le risque d'erreurs de transcription dans les chaînes de factorisation.
Équivalences théoriques : La formalisation prouve l'équivalence entre la formulation fonctionnelle de la conjecture et sa reformulation en théorie des ensembles (que l'ensemble des nombres premiers est « surnaturel », signifiant qu'il ne contient aucun sous-ensemble naturel infini).
Conséquences : Sous réserve de la conjecture, la formalisation prouve que l'ensemble des nombres de Fermat composés est infini et que l'ensemble des valeurs non-premières pour toute fonction naturelle non constante est infini.

Signification
L'article affirme que sa principale importance réside dans la rigueur et l'exhaustivité de la formalisation. Il transforme un « défi difficile pour n'importe quel type d'intelligence » (tel que décrit dans [3]) en une cible précise et vérifiable par machine. En éliminant toute ambiguïté et en s'assurant que chaque étape est vérifiée par le noyau de Lean, ce travail permet aux systèmes de raisonnement automatisés de tenter une preuve de la conjecture sans risque d'erreur humaine dans les définitions sous-jacentes. L'article ne prétend pas résoudre la conjecture, mais vise plutôt à fournir l'infrastructure nécessaire pour que toute solution puisse être validée. Il démontre également la faisabilité de la formalisation de conjectures complexes de théorie des nombres, basées sur l'expérimentation, au sein de l'écosystème Mathlib.

Articles similaires