Cette page présente mes activités de formalisation de preuves mathématiques, réalisées avec le logiciel Lean et la librairie Mathlib. La liste complète de mes contributions à Mathlib est disponible sur GitHub.
Théorème des unités de Dirichlet
Xavier Roblot
Description Formalisation du théorème des unités de Dirichlet : le groupe des unités \((\mathcal{O}_K)^\times\) de l'anneau des entiers d'un corps de nombres \(K\), modulo son sous-groupe de torsion, est un \(\mathbb{Z}\)-module libre de rang \(r_1 + r_2 - 1\), où \(r_1\) et \(r_2\) désignent respectivement le nombre de plongements réels et le nombre de paires de plongements complexes conjugués. La preuve repose sur le plongement logarithmique et la théorie des \(\mathbb{Z}\)-réseaux.
Mathlib Voir dans Mathlib
Théorèmes de Hermite et Hermite-Minkowski
Xavier Roblot
Description Formalisation de deux résultats classiques sur le discriminant des corps de nombres. Le théorème de Hermite-Minkowski affirme que tout corps de nombres non trivial vérifie \(|\mathrm{disc}(K)| > 2\) ; en particulier, tout corps de nombres admet une ramification. Le théorème de Hermite stipule qu'il n'existe qu'un nombre fini de corps de nombres (à isomorphisme près) de discriminant borné. La preuve repose sur les méthodes géométriques de Minkowski et sur le plongement mixte du corps de nombres.
Mathlib Voir dans Mathlib
Formule analytique du nombre de classes
Xavier Roblot
Description Formalisation de la formule analytique du nombre de classes, aussi connue sous le nom de formule de Dirichlet. La fonction zêta de Dedekind \(\zeta_K(s)\) est définie comme la série de Dirichlet dont les coefficients comptent les idéaux de norme donnée. La formalisation établit le calcul de la limite \(\lim_{s \to 1^+} (s-1)\,\zeta_K(s) = 2^{r_1}(2\pi)^{r_2} \mathrm{Reg}(K)\, h(K) / (w\, \sqrt{|\mathrm{disc}(K)|})\), où \(h(K)\) est le nombre de classes, \(\mathrm{Reg}(K)\) le régulateur, \(w\) le nombre de racines de l'unité, et \(r_1, r_2\) les nombres de plongements réels et complexes.
Mathlib Voir dans Mathlib
Volume des boules \(\ell^p\) dans Mathlib
Xavier Roblot, 2026
Description Nous décrivons la formalisation dans Mathlib de formules explicites pour le volume des boules \(\ell^p\), aussi bien dans \(\mathbb{R}^n\) que dans \(\mathbb{C}^n\), pour tout réel \(p \geq 1\). Plutôt que de traiter chaque cas séparément, toutes les formules se déduisent d'une identité unique exprimant le volume de la boule unité en termes d'une intégrale de type gaussien et de la fonction Gamma. Cette approche abstraite, valable pour tout espace normé de dimension finie muni d'une mesure de Haar, couvre également les espaces mélangeant coordonnées réelles et complexes, cas qui apparaît en théorie algébrique des nombres et qui était d'ailleurs la motivation initiale de ce travail.
Prépublication HAL