Ce papier ne prouve pas l’hypothèse de Riemann. Il fait quelque chose de différent : il trace un chemin complet depuis une observation algébrique finie jusqu’aux limites structurelles des approches spectrales, identifiant précisément ce qui fonctionne, ce qui échoue, et pourquoi.
Enoncé fondateur
« Nous construisons un noyau spectral fini (dimension 7) décrivant la structure modulaire des nombres premiers, et explorons son extension vers une théorie analytique de type zêta, encore ouverte. »
Classification mod 30, profil spectral, λ = 1/√7, Parseval, tour primorielle
Prouvé · Lean 4 certifié
Trois barrières No-Go, obstruction de résonance additive
Prouvé analytiquement
Métrique logarithmique, divergence de résonance, quasi-continuum
Prouvé asymptotiquement
Correspondance de trace, déterminant spectral
Conditionnel
Ce programme distingue quatre niveaux épistémiques, et ne les mélange jamais :
C’est la phrase canonique du programme. La confusion entre ces trois niveaux est la cause première des fausses preuves dans l’histoire de la théorie analytique des nombres.
Chaque résultat porte son statut. Un résultat [M] ne devient jamais [D] par accumulation de données. Un résultat [C] ne devient jamais [D] sans fermer ses hypothèses. Cette discipline est encodée dans le code Lean lui-même.
La légende épistémique est stricte : proved → [D] = certifié Lean 4 ou prouvé par théorie des caractères ; verified → [M] = confirmé numériquement ; negative → [F] = résultat d’impossibilité ; conditional → [C] = dépend d’hypothèses explicites non vérifiées.
Ce que nous revendiquons : une architecture dont chaque étage est étiqueté, testable et falsifiable.
Positionnement · paysage 2026
La séquence est instructive, et elle valide la discipline du programme mieux qu’aucun argument. À l’automne 2025, plusieurs annonces de « problèmes d’Erdős résolus par IA » ont circulé — puis se sont révélées être des recherches documentaires : le modèle avait retrouvé des articles publiés que le mainteneur de la base ignorait, non produit un argument nouveau. En janvier 2026, les succès ont été d’une autre nature : des arguments originaux, non documentés auparavant, et surtout vérifiés formellement en Lean.
Ce qui a distingué les seconds des premiers n’est pas l’éloquence : c’est l’existence d’un certificat vérifiable. Lean impose la rigueur au niveau de la logique symbolique ; toute lacune fait rejeter la preuve. C’est précisément la fonction que le programme assigne à sa couche Lean, à son registre de statuts et à sa règle centrale : une trace séduisante ne « monte » pas d’elle-même — elle doit être attestable.
1. Découper les intuitions en énoncés vérifiables. Dans le régime IA–Lean, une intuition en langage naturel n’a de valeur qu’une fois découpée en lemmes qu’un assistant peut contrôler. Le programme fait de même : chaque relief, chaque triplet, chaque no-go est ramené à un énoncé fini, calculable ou formalisable — le lemme de double admissibilité de T_C, le no-go C-031, la borne KLMN. On ne publie pas une idée ; on publie un énoncé avec son statut.
2. Séparer les statuts. Le régime IA–Lean distingue nettement ce qui est prouvé (vérifié en Lean, accepté par un expert) de ce qui est conjecture ou heuristique. Le programme tient la même séparation, explicitement : démontré [D], mesuré [M], heuristique [H], conditionnel [C], ouvert [O], réfuté [F]. Une idée ne change de statut que si elle y a droit — et le Journal F consigne, datées, celles qui sont tombées.
3. Confier à la machine l’attestation, pas l’autorité. Dans les résolutions d’Erdős, Lean atteste la validité locale, mais c’est un mathématicien qui accepte la portée du résultat — Terence Tao, par exemple, qui situe d’ailleurs ces succès dans la « longue traîne » des problèmes, non parmi les grands murs. Le programme inscrit la même limite dans sa règle fondatrice : la machine atteste ; l’humain statue. Le dispositif InterIA fait travailler plusieurs modèles, mais « le plus prudent gagne », et aucune machine ne décide de la portée.
Depuis 2026, la recherche mathématique assistée par IA connaît un changement de régime : certains systèmes ne se contentent plus de produire des raisonnements plausibles en langage naturel ; ils cherchent à produire des preuves formelles vérifiables par un assistant comme Lean.
Des résultats récents autour de problèmes d’Erdős ont rendu ce changement visible. Le point important n’est pas que « l’IA fait des mathématiques » au sens vague, mais que des énoncés précis peuvent désormais être proposés, découpés, formalisés, vérifiés mécaniquement, puis restitués aux mathématiciens sous forme lisible.
Couret–Unification se situe dans ce paysage avec prudence.
Le programme ne revendique pas le même statut que ces résultats fermés. Il n’affirme pas avoir résolu l’hypothèse de Riemann, ni franchi les verrous globaux du front Hilbert–Pólya. La formule de trace reste un mur. Les verrous fonctionnel, eulérien, archimédien et spectral restent explicitement ouverts.
La proximité est donc méthodologique, non triomphale.
Trois exigences partagées avec ce nouveau régime
C’est le sens du dispositif InterIA, du registre de claims, de la formalisation Lean et de la règle centrale du programme :
La position exacte du programme
Nous ne captons pas leur lumière ; nous acceptons leur exigence.