Publié à l’origine sur giftheory.substack.com
13 théorèmes, zéro confiance requise
GIFT rencontre Lean 4
3 décembre 2025
« Prouve-le. »
C’est de bonne guerre.
GIFT est désormais vérifié en Lean 4. 13 relations exactes dérivées de la topologie, contrôlées par un assistant de preuve. Zéro sorry. Seulement les axiomes standards. L’arithmétique compile.
Vous n’avez pas à faire confiance aux maths. Lean les a vérifiées.
Le problème du papier crayon
La physique théorique a un petit souci de reproductibilité, qu’on tait souvent. Pas de la fraude, juste de la complexité. Les dérivations s’étalent sur des pages. Les indices se multiplient. Les erreurs de signes se dissimulent. Un facteur 2 qui se glisse quelque part vers l’équation 47.
La relecture par les pairs attrape certaines erreurs. Mais les relecteurs sont humains, occupés, et redériventt rarement tout depuis le début. Résultat : les articles sont publiés, les erreurs persistent, et des années plus tard quelqu’un trouve un signe moins qui change tout.
Et si une machine vérifiait chaque étape ?
Entrée en scène de Lean
Lean est un assistant de preuve : un logiciel qui vérifie les preuves mathématiques jusqu’aux axiomes fondationnels. Si un théorème compile, il est correct. Pas d’ambiguïté. Pas de « croyez-moi sur parole ».
La communauté Lean l’utilise pour formaliser des mathématiques sérieuses : la bibliothèque Mathlib couvre des milliers de théorèmes, des contributeurs travaillent à formaliser le dernier théorème de Fermat, et des médaillés Fields la prennent au sérieux.
La question était simple : peut-on formaliser les relations centrales de GIFT ? Pas l’interprétation physique, juste l’arithmétique. Les chiffres tombent-ils vraiment juste ?
Ce que la formalisation prouve
GIFT affirme que les constantes physiques émergent des invariants topologiques. La formalisation Lean vérifie un énoncé précis :
SI les entiers suivants sont fixés :
- dim(E₈) = 248
- b₂(K₇) = 21
- b₃(K₇) = 77
- dim(G₂) = 14
- dim(J₃(𝕆)) = 27
ALORS ces relations exactes tiennent :
| Relation | Formule | Valeur | Preuve |
|---|---|---|---|
| sin²θ_W | b₂ / (b₃ + dim G₂) | 3/13 | norm_num |
| τ | (496 × 21) / (27 × 99) | 3472/891 | norm_num |
| det(g) | (5 × 13) / 32 | 65/32 | norm_num |
| κ_T | 1 / (77 − 14 − 2) | 1/61 | norm_num |
| δ_CP | 7 × 14 + 99 | 197° | rfl |
| m_τ/m_e | 7 + 10×248 + 10×99 | 3477 | rfl |
| m_s/m_d | 4 × 5 | 20 | rfl |
| Q_Koide | 14 / 21 | 2/3 | norm_num |
| numérateur λ_H | 14 + 3 | 17 | rfl |
| H* | 21 + 77 + 1 | 99 | rfl |
| p₂ | 14 / 7 | 2 | rfl |
| N_gen | topologique | 3 | rfl |
| dim(E₈×E₈) | 2 × 248 | 496 | rfl |
Chaque relation a son propre théorème autonome. Chaque théorème compile. Le théorème principal regroupe les 13 :
theorem GIFT_framework_certified (G : GIFTStructure)
(h : is_zero_parameter G) :
(G.b2 : ℚ) / (G.b3 + G.dim_G2) = 3 / 13 ∧
(G.dim_E8xE8 * G.b2 : ℚ) / (G.dim_J3O * G.H_star) = 3472 / 891 ∧
-- ... 11 conjonctions de plus
G.dim_E8xE8 = 496 := by
obtain ⟨he, hr, hw, hk, hb2, hb3, hg, hj⟩ := h
refine ⟨?_, ?_, ?_, ...⟩ <;> simp_all <;> norm_num
Audit des axiomes
Question naturelle : sur quels axiomes la preuve repose-t-elle ? Des hypothèses cachées pourraient ruiner l’édifice.
#print axioms GIFT_framework_certified
-- [propext, Quot.sound]
Deux axiomes. Tous deux sont des fondations standards de Lean :
| Axiome | Description | Statut |
|---|---|---|
| propext | Extensionnalité propositionnelle | standard |
| Quot.sound | Robustesse des quotients | standard |
Aucun axiome de physique. Aucune hypothèse spécifique au domaine. La preuve est de l’arithmétique pure à partir d’entiers fixés.
Ce que la formalisation NE prouve PAS
La clarté importe. Le code Lean prouve :
SI ces entiers topologiques, ALORS ces rapports.
Il ne prouve pas le SI. L’affirmation que b₂(K₇) = 21 et b₃(K₇) = 77 sont les bonnes valeurs pour notre univers, c’est de la physique, pas des mathématiques. Cette affirmation est empirique et falsifiable.
Les expériences la testeront :
| Prédiction | Valeur | Expérience | Calendrier |
|---|---|---|---|
| δ_CP | 197° | DUNE, Hyper-K | 2027-2030 |
| sin²θ_W | 3/13 = 0,23077 | FCC-ee | 2040s |
| κ_T | 1/61 | DESI | 2025-2027 |
Si DUNE mesure δ_CP = 250° ± 10°, le cadre est falsifié. Pas de réinterprétation. Pas d’ajustement de paramètre. Mort.
La formalisation Lean ne protège pas contre cela. Elle garantit seulement : si la topologie est juste, l’arithmétique est juste.
Structure du dépôt
La formalisation est modulaire :
Lean/
├── GIFT/
│ ├── Algebra/ # système de racines de E₈, groupe de Weyl, représentations
│ ├── Geometry/ # holonomie G₂, construction TCS
│ ├── Topology/ # nombres de Betti, cohomologie
│ ├── Relations/ # jauge, neutrino, quark, lepton, Higgs, cosmologie
│ └── Certificate/ # théorèmes principaux, audit des axiomes
17 modules. ~2000 lignes de Lean. Chaque secteur (jauge, neutrino, quark, etc.) a son propre fichier avec des théorèmes autonomes.
Construisez-le vous-même :
git clone https://github.com/gift-framework/GIFT.git
cd GIFT/Lean
lake update
lake exe cache get # Téléchargement du cache Mathlib (~2 Go)
lake build # ~5 min avec le cache
Ou lisez simplement les preuves. Elles sont courtes. La plupart tiennent en une ligne.
Pourquoi c’est important
La vérification formelle n’est pas courante en physique théorique. La plupart des articles s’appuient sur la relecture par les pairs et la réputation. Mais une preuve est une preuve, elle ne devrait pas dépendre de qui l’a écrite.
La formalisation Lean crée un précédent :
- Reproductibilité : n’importe qui peut vérifier l’arithmétique. Cloner, construire, vérifier.
- Transparence : pas d’hypothèses cachées. Les axiomes sont listés.
- Précision : 3/13 signifie exactement 3/13, pas « environ 0,231 ».
Cela ne convaincra personne que GIFT est de la physique correcte. C’est à cela que servent les expériences. Mais cela élimine une classe entière d’objections : l’arithmétique n’est pas fausse. Lean l’a vérifiée.
Conclusion
13 théorèmes. Zéro sorry. Seulement des axiomes standards.
Les relations entre invariants topologiques et constantes physiques sont désormais vérifiées par machine. Les dérivations ne sont pas des approximations ou des ajustements : c’est de l’arithmétique rationnelle exacte, prouvée à partir d’entiers fixés.
La physique reste à tester. Les maths sont réglées.
Dépôt : https://github.com/gift-framework/core/
Retours, corrections, et critiques brutales bienvenus via les issues GitHub.