💻 computer science

ZFLean: a framework for set-level mathematics in Lean

L'article présente ZFLean, une bibliothèque Lean 4 qui intègre la théorie des ensembles ZFC fondamentale dans l'écosystème Mathlib avec une ergonomie améliorée, des constructions canoniques et des ponts vers des types natifs pour faciliter les preuves mixtes au niveau des ensembles et typées.

Auteurs originaux : Vincent Trélat

Publié 2026-04-28

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Vincent Trélat

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 que vous essayez de construire une maison. Vous avez deux ensembles différents de plans et d'outils :

Les outils « Typés » (le système natif de Lean) : Ils sont comme des bras robotisés haute technologie guidés par laser. Ils sont incroyablement précis, mais ils ne fonctionnent que si chaque brique est parfaitement étiquetée avec son type spécifique (par exemple, « Brique Rouge », « Brique Bleue »). Si vous essayez d'utiliser une « Brique Rouge » là où une « Brique Bleue » est requise, le robot s'arrête et refuse de travailler. C'est excellent pour la sécurité, mais parfois les mathématiques semblent avoir besoin d'être plus flexibles.
Les outils « Ensembles » (ZFC) : Ils sont comme un immense tas désordonné d'argile brute. Dans ce monde, tout est simplement « de la matière ». Vous pouvez façonner un morceau d'argile en une tasse, une boule ou un carré, et tout cela reste simplement « de l'argile ». C'est ainsi que les mathématiciens traditionnels pensent souvent aux ensembles : tout est un élément d'une collection, et vous pouvez mélanger et assortir librement.

Le Problème :
Pendant longtemps, si vous vouliez faire des mathématiques en utilisant les outils « Ensembles » à l'intérieur de l'atelier robotisé « Typé », c'était un cauchemar. Vous deviez constamment traduire vos formes en argile en étiquettes compatibles avec les robots, prouver que votre traduction était correcte, puis traduire les résultats à nouveau. C'était lent, ennuyeux et sujet aux erreurs. La plupart des gens évitaient simplement le tas d'argile et s'en tenaient aux robots.

La Solution : ZFLean
Vincent Trélat a créé ZFLean, qui équivaut à construire un traducteur universel et un ensemble d'outils personnalisés directement à l'intérieur de l'atelier robotisé.

Voici comment cela fonctionne, en utilisant des analogies simples :

1. L'atelier « Argile » (Le modèle ZFC)

ZFLean établit une zone spéciale à l'intérieur de l'atelier robotisé où les règles de « l'argile » s'appliquent. Ici, vous pouvez définir des ensembles, des relations et des fonctions exactement comme le ferait un mathématicien traditionnel, sans vous soucier des « types » stricts que le robot exige habituellement. C'est un espace sûr où vous pouvez dire : « Ceci est un ensemble de nombres », sans que le robot ne demande : « Est-ce un Nat ou un Int ? »

2. Le « Traducteur Intelligent » (Le calcul relationnel)

Le plus gros problème des anciens jours était le « boilerplate » — la paperasse répétitive et ennuyeuse requise pour prouver que vos formes en argile étaient effectivement valides.

L'ancienne méthode : Vous deviez prouver manuellement, « Oui, cette relation est une fonction », et « Oui, ce domaine est valide », pour chaque étape individuelle.
La méthode ZFLean : Le cadre est livré avec de petits assistants intelligents (appelés tactiques comme zrel, zpfun et zfun). Imaginez-les comme des formulaires de remplissage automatique. Lorsque vous écrivez une preuve, ces assistants vérifient automatiquement les détails ennuyeux et remplissent la paperasse pour vous. Vous écrivez les mathématiques ; les assistants gèrent la charge administrative.

3. Le « Pont » (Interopérabilité)

C'est la partie magique. Habituellement, le monde de « l'argile » et le monde du « robot » étaient séparés. ZFLean construit des ponts entre eux.

Si vous construisez un ensemble de nombres naturels dans le monde de l'argile, ZFLean peut instantanément dire : « Hé, c'est en fait la même chose que le type Nat du robot. »
Cela signifie que vous pouvez faire vos mathématiques d'ensemble théoriques désordonnées et flexibles, puis traverser sans heurt le pont pour utiliser les outils puissants et préfabriqués du robot (comme les solveurs algébriques) pour terminer le travail. Vous n'avez pas à choisir l'un ou l'autre ; vous pouvez utiliser les deux dans la même preuve.

4. Le « Kit de Lego » (Constructions canoniques)

Pour faciliter la vie, ZFLean est livré avec un kit préfabriqué de pièces de Lego standard.

Besoin d'un ensemble de valeurs Vrai/Faux ? Voici un ensemble Booléen.
Besoin d'un ensemble de nombres comptables ? Voici un ensemble de Nombres Naturels.
Besoin d'un moyen de gérer des valeurs « peut-être » (comme une option) ? Voici un ensemble Option.
Ce ne sont pas simplement de l'argile brute ; ils sont pré-moulés, testés et accompagnés d'instructions sur leur utilisation (comme « comment additionner deux nombres » ou « comment actionner un interrupteur »).

5. L'« Essai sur route » (L'étude de cas)

Pour prouver que ce système fonctionne, l'auteur l'a testé avec une énigme mathématique classique appelée l'isomorphisme de Curry.

Imaginez ceci : Vous avez une machine qui prend deux entrées à la fois (comme une machine à sandwich qui prend du pain et de la viande). Le « Curry » est le processus consistant à transformer cela en une machine qui prend une entrée (pain) et ensuite vous donne une nouvelle machine qui prend la deuxième entrée (viande).
L'auteur a utilisé ZFLean pour prouver que ces deux façons de penser à la machine sont en fait la même chose. Le script de preuve ressemblait presque exactement à un mathématicien humain l'écrivant sur un tableau noir, les « assistants intelligents » gérant silencieusement tous les bugs techniques en arrière-plan.

La Conclusion

ZFLean est un cadre qui permet aux mathématiciens de travailler dans le style flexible et intuitif de la théorie des ensembles traditionnelle (l'« argile ») tout en vivant à l'intérieur d'un système moderne et rigoureux de preuves informatiques (les « robots »). Il élimine les frictions de la traduction, automatise la paperasse ennuyeuse et construit des ponts afin que vous puissiez utiliser les meilleurs outils des deux mondes sans rester coincé au milieu.

Le résultat est une bibliothèque d'environ 8 300 lignes de code qui rend la réalisation de mathématiques au « niveau ensemble » dans Lean aussi naturelle et fluide que de l'écrire sur du papier.

1. Énoncé du problème

La formalisation moderne dans les assistants de preuve comme Lean est principalement basée sur la théorie des types (spécifiquement la théorie des types dépendants), où les objets mathématiques sont des types construits. Bien que puissante, cette approche peut être lourde pour les mathématiques au niveau des ensembles (ZFC), qui sont souvent préférées pour :

Le raisonnement extensionnel : raisonner sur l'égalité basée sur les éléments plutôt que sur la construction.
La partialité : gérer les fonctions partielles naturellement via des relations plutôt que de les encoder avec des types Option ou des types dépendants.
Le raisonnement de style catégorie : travailler "à isomorphisme près" plutôt que selon une égalité définitionnelle stricte.

Le défi : Travailler directement dans un modèle théorique des ensembles au sein d'un assistant typé (comme le modèle ZFC de Mathlib dans Lean) introduit une friction significative :

Code répétitif (Boilerplate) : Les utilisateurs doivent constamment gérer manuellement des "conditions secondaires" (par exemple, prouver qu'une relation est bien définie, prouver qu'une fonction est totale).
Fragilité : Franchir la frontière entre les objets théoriques des ensembles (ZFSet) et les types natifs de Lean (Type) est manuel et sujet aux erreurs.
Manque d'automatisation : Les outils existants manquent souvent des indices de réécriture et des tactiques spécifiques nécessaires pour rendre les preuves théoriques des ensembles aussi fluides que les preuves typées.

2. Méthodologie

L'auteur présente ZFLean, une bibliothèque Lean 4 construite sur le modèle ZFC existant de Mathlib. La méthodologie se concentre sur la création d'un calcul relationnel uniforme et de ponts d'interopérabilité pour rendre le développement au niveau des ensembles ergonomique.

Choix de conception fondamentaux :

Fondation : S'appuie sur l'implémentation de ZFC de Mathlib, qui construit les ensembles comme le quotient extensionnel de "pré-ensembles" (PSet) inductifs.
Calcul relationnel : Au lieu de traiter les fonctions comme des objets totaux de premier ordre (comme dans la théorie des types standard), ZFLean les traite comme des relations fonctionnelles. Il introduit un calcul pour les relations binaires, les fonctions partielles et les fonctions totales.
Automatisation via tactiques : Le cadre introduit trois tactiques légères (zrel, zpfun, zfun) conçues pour décharger automatiquement les conditions secondaires de bonne formation (par exemple, prouver qu'une composition est une relation ou une fonction).
Ponts : La bibliothèque construit des isomorphismes explicites (ponts) entre les objets canoniques ZFC (par exemple, ZFBool, ZFNat) et les types natifs de Lean (Bool, Nat), permettant de transporter les propriétés entre les deux mondes.

3. Contributions clés

A. Calcul relationnel et automatisation

Définitions : Formalise la converse, l'identité, la composition, le domaine, l'image et l'image directe pour les relations.
Fonctionnalité : Distingue les fonctions partielles (IsPFunc) des fonctions totales (IsFunc).
Tactiques :
- zrel : Décharge les objectifs prouvant qu'un ensemble est une relation ( $R \subseteq A \times B$ ).
- zpfun : Décharge les objectifs prouvant qu'un ensemble est une fonction partielle.
- zfun : Décharge les objectifs prouvant qu'un ensemble est une fonction totale.
- Ces tactiques utilisent des lemmes étiquetés par des attributs (par exemple, @[zfun]) pour résoudre récursivement les conditions secondaires, masquant le code répétitif à l'utilisateur.
Notation : Introduit une syntaxe pratique pour l'application de fonction (@zf(x)) et l'abstraction $\lambda$ , avec des théorèmes pour la $\beta$ -réduction, l'expansion $\eta$ et l'extensionnalité.

B. Constructions canoniques

La bibliothèque fournit une suite d'objets mathématiques standards définis dans ZFC, complets avec leurs propriétés universelles :

Booléens : Un ensemble à deux éléments $B$ avec une structure algébrique (conjonction, disjonction, négation) et un éliminateur de cas.
Nombres entiers naturels ( $\mathbb{N}$ ) : Définis comme le plus petit ensemble inductif (ordinaux de von Neumann). Comprend un récenseur, un principe d'induction et des opérations arithmétiques. Crucialement, il est équipé d'une structure CommSemiring pour exploiter la tactique ring de Lean.
Entiers relatifs ( $\mathbb{Z}$ ) et rationnels ( $\mathbb{Q}$ ) : Construits comme des types quotients de paires de naturels/entiers, avec des opérations relevées depuis les représentants.
Coproduits et Options : Définitions théoriques des ensembles des types somme et des types option.

C. Isomorphismes et transport

Plongements et isomorphismes : Définit les plongements au niveau des ensembles ( $A \hookrightarrow_z B$ ) et les isomorphismes ( $A \cong_z B$ ) via des fonctions injectives et bijectives.
Théorème de Cantor-Schröder-Bernstein : Formalisé dans le cadre.
Transport : Prouve que les constructions ZFC sont isomorphes aux types natifs de Lean (par exemple, ZFBool $\simeq$ Bool). Cela permet aux utilisateurs de "transporter" les théorèmes de la riche bibliothèque théorique des types de Mathlib vers le contexte théorique des ensembles de manière transparente.

D. Étude de cas : Isomorphisme de currying

Le papier démontre l'utilité du cadre en prouvant l'isomorphisme de currying : $C^{A \times B} \cong (C^B)^A$ .

La preuve définit curryz et uncurryz comme des fonctions au niveau des ensembles.
Elle prouve qu'ils sont des inverses mutuels en utilisant l'automatisation du cadre pour gérer les conditions secondaires (bonne définition des compositions et des images).
Le script de preuve reflète étroitement les arguments mathématiques standards, la couche d'automatisation gérant la "vérification théorique des ensembles ennuyeuse".

4. Résultats

Taille de l'artefact : La bibliothèque se compose de 8 324 lignes de code Lean et de 706 théorèmes prouvés.
Répartition des composants :
- Calcul relationnel : ~2 534 lignes de code (172 théorèmes).
- Naturels : ~1 260 lignes de code (199 théorèmes).
- Plongements/Isomorphismes : ~1 626 lignes de code (31 théorèmes).
Utilisabilité : L'étude de cas démontre que le cadre réduit avec succès la friction de la formalisation au niveau des ensembles. Les utilisateurs peuvent écrire des preuves qui ressemblent à des arguments théoriques des ensembles standards sans prouver manuellement que chaque composition de relations est une relation valide.
Interopérabilité : La capacité à basculer entre ZFSet et Type natif permet de réutiliser les tactiques algébriques de Mathlib (comme ring) sur des objets théoriques des ensembles.

5. Importance

Réconciliation des fondations : ZFLean réconcilie efficacement les vues "théorie des ensembles" et "théorie des types" des mathématiques au sein d'un seul assistant de preuve. Il permet aux mathématiciens de choisir le fondement le plus naturel pour un problème spécifique (ensembles extensionnels vs types constructifs) sans perdre l'accès à l'automatisation de l'écosystème.
Ergonomie : En automatisant les conditions secondaires fastidieuses inhérentes à la théorie des ensembles (preuves d'appartenance, bonne définition des relations), il rend le développement ZFC dans Lean viable pour les non-experts et pratique pour la formalisation à grande échelle.
Extensibilité : La conception modulaire (calcul relationnel + objets canoniques + ponts) permet une extension facile. Les travaux futurs incluent la formalisation des nombres réels (via des suites de Cauchy ou des coupures de Dedekind) et de l'analyse de base.
Comparaison : Contrairement à Isabelle/ZF (où la théorie des ensembles est un objet logique séparé) ou aux développements théoriques des ensembles de Rocq (qui manquent souvent d'intégration profonde avec l'automatisation théorique des types), ZFLean offre une approche hybride qui maintient les preuves au niveau des ensembles tout en exploitant l'infrastructure native théorique des types de Lean.

En conclusion, ZFLean fournit un cadre robuste, ergonomique et interopérable pour réaliser les mathématiques fondamentales en ZFC dans Lean 4, réduisant avec succès la barrière à l'entrée pour la formalisation théorique des ensembles tout en maintenant la compatibilité avec l'écosystème plus large de Mathlib.