Contexte et objectif

Le dépôt PrimeGaps186 propose une formalisation en Lean 4 d’une borne sur les écarts entre nombres premiers, spécifiquement que tout écart est inférieur ou égal à 186. Le résultat repose sur trois axiomes explicites : kloosterman3_bound, kloosterman2_correlation_bound et physical_integral_bounds. Ces axiomes traduisent des estimations issues de la théorie analytique des nombres, notamment le théorème de Deligne sur les sommes de Kloosterman et les travaux de Fouvry‑Kowalski‑Michel sur les sommes de caractères.

Architecture de la preuve Lean

Le projet utilise Lean 4.34.0‑rc2 et les bibliothèques Mathlib correspondantes. Le fichier principal PrimeGaps186.lean définit le namespace PrimeGap186 et expose les déclarations essentielles. La preuve conditionnelle s’appuie sur les axiomes suivants :

axiom PrimeGap186.kloosterman3_bound : ∀ p : ℕ, prime p → …
axiom PrimeGap186.kloosterman2_correlation_bound : ∀ p : ℕ, prime p → …
axiom PrimeGap186.physical_integral_bounds : …

Le premier axiome invoque le théorème 4.1.1(1)‑(2) de Katz (1988), qui découle du résultat de Deligne sur les sommes de Kloosterman. Le second se fonde sur la Proposition 2 du texte de Fouvry, Kowalski et Michel (2013). Le troisième regroupe 104 bornes extérieures et 45 intérieures, ainsi que trois bornes de cap, toutes issues de calculs numériques non formalisés. La chaîne de dépendances montre que, bien que le noyau Lean accepte la construction, la validité mathématique dépend entièrement de la véracité de ces entrées externes.

Certificat numérique Python

Un script Python recompute les bornes à partir de zéro. L’environnement reproduit exactement les versions suivantes : Python 3.12.13, NumPy 2.2.6, python‑flint 0.9.0 et une version personnalisée de FLINT 3.6.0 avec correction de la convolution polynomiale signée. Le lancement s’effectue avec la commande :

python3 -B prime_gap_186_certificate.py --workers 4 --output prime_gap_186_fresh.json

Le script impose que les options d’optimisation Python (PYTHONOPTIMIZE) restent désactivées et que les vérifications de précision flottante et de convolution signée réussissent. Un résultat « passed: true » indique que les calculs numériques concordent avec les valeurs attendues, mais il ne constitue pas une preuve formelle dans Lean : les axiomes restent non démontrés.

Analyse des limites et perspectives

La formalisation illustre la capacité actuelle de Lean à encapsuler des arguments de théorie analytique, mais elle met en évidence une fracture entre preuve formelle et calcul numérique. Pour transformer la preuve conditionnelle en preuve absolue, il faudrait :

1. Formaliser le théorème de Deligne sur les sommes de Kloosterman dans Mathlib, ce qui impliquerait de développer la théorie des motifs et des poids dans un cadre constructif.

2. Intégrer les résultats de Fouvry‑Kowalski‑Michel, notamment la borne de corrélation, en traduisant leurs arguments de la méthode du cercle dans Lean.

3. Vérifier les 149 bornes numériques (104 + 45) à l’aide d’une extraction certifiée, par exemple en utilisant un compilateur de code vérifié comme CompCert ou en recourant à des preuves de calculs dans Coq/Lean via des certificats de type proof‑carrying code.

En l’état, le projet reste une démonstration de concept : il montre que la chaîne de dépendances peut être rendue explicite, mais la confiance repose sur la rigueur des publications citées et sur la reproductibilité du certificat Python. La prochaine étape pour la communauté de la vérification formelle sera de réduire ces dépendances externes, afin d’obtenir une preuve entièrement vérifiable par le noyau Lean.