💻 computer science

Rzk: a Proof Assistant for Synthetic $\infty$ -Categories

Cet article présente Rzk, un assistant de preuve pratique implémentant une variante raffinée et computationnelle de la théorie des types simpliciaux de Riehl et Shulman afin de permettre le raisonnement synthétique sur les $\infty$ -catégories, tout en établissant sa fidélité et sa conservativité par rapport à la théorie originale et en fournissant un tutoriel sur son usage et son implémentation.

Auteurs originaux : Nikolai Kudasov, Violetta Sim, Benedikt Ahrens

Publié 2026-07-15

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Nikolai Kudasov, Violetta Sim, Benedikt Ahrens

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 l'univers des mathématiques comme un terrain de jeu géant et infini. Pendant longtemps, le jeu le plus populaire ici était la Théorie des Types d'Homotopie (HoTT). Dans ce jeu, tout est fait de « formes » parfaitement flexibles. Si vous avez un chemin d'un point A vers un point B, vous pouvez toujours le parcourir en marche arrière. C'est comme un monde d'élastiques où chaque étirement peut être ramené à son état d'origine. C'est excellent pour étudier les « espaces » (des objets mathématiques où tout est réversible), mais c'est un peu trop parfait pour le monde désordonné des catégories où certains chemins sont des rues à sens unique.

Entrez dans Rzk, un nouvel assistant de preuve construit par Nikolai Kudasov, Violetta Sim et Benedikt Ahrens. Considérez Rzk comme un kit de construction spécialisé conçu pour bâtir des formes dirigées. Dans ce nouveau terrain de jeu, vous pouvez avoir un chemin de A vers B qui ne peut pas être parcouru en marche arrière. C'est comme construire avec des briques LEGO où certaines connexions sont permanentes : vous pouvez emboîter une pièce, mais vous ne pouvez pas la déclipser sans casser le modèle. Cela permet aux mathématiciens de raisonner sur les $\infty$ -catégories, des structures complexes où les flèches (morphismes) ont des directions et ne sont pas toujours réversibles.

La Grande Idée : Une Nouvelle Façon de Construire

Le papier présente Rzk comme un outil qui implémente une théorie spécifique appelée Théorie des Types Simpliciaux (RSTT), initialement proposée par Emily Riehl et Michael Shulman.

Voici l'astuce ingénieuse utilisée par Rzk :
Dans la théorie originale (RSTT), il y avait une « boîte magique » spéciale appelée type d'extension. Cette boîte vous permettait de définir une fonction qui se comporte d'une certaine manière sur les arêtes d'une forme (comme un triangle) et fait ce qu'elle veut au milieu. C'était puissant, mais un peu comme une boîte noire ; les règles de son fonctionnement étaient parfois cachées dans les petits caractères.

Rzk prend cette boîte magique et la ouvre en deux.

La Forme : Il sépare la partie « forme » (le triangle ou l'intervalle) de la partie « bordure » (les règles pour les arêtes).
Les Règles : Il introduit une nouvelle règle explicite appelée sous-typage sans coercition. Imaginez que vous avez une voiture miniature qui rentre dans une petite boîte. Dans l'ancien système, le système supposait simplement que la voiture rentrait dans une boîte plus grande sans vérifier. Dans Rzk, le système vérifie explicitement que la voiture rentre, mais il ne vous force pas à emballer la voiture dans un emballage supplémentaire (une « coercition ») pour la faire entrer. Il dit simplement : « Oui, cette voiture est aussi un jouet, donc elle appartient à la boîte de jouets. » Cela rend la logique plus propre et plus facile à vérifier pour les ordinateurs.

Ce que Rzk Peut Faire (et Ne Peut Pas Faire)

Les auteurs ont construit une « bibliothèque standard » pour ce nouveau système appelée sHoTT. Elle est déjà massive, contenant plus de 25 000 lignes de code et près de 1 500 déclarations de haut niveau. Cette bibliothèque a réussi à formaliser des concepts complexes comme le lemme de Yoneda $\infty$ -catégorique (un théorème fondamental en théorie des catégories) et divers types de « fibrations » (façons d'empiler des catégories les unes sur les autres).

Cependant, le papier est très prudent sur ce qu'il prétend avoir prouvé :

Il est Fidèle : Les auteurs ont prouvé que tout ce que vous pouvez prouver dans la théorie originale (RSTT) peut aussi être prouvé dans Rzk. C'est une traduction parfaite.
Il est Conservatif (avec une réserve) : Ils ont prouvé que Rzk n'invente aucune nouvelle vérité sur l'ancienne théorie. Si Rzk prouve quelque chose sur une ancienne forme, l'ancienne théorie aurait pu le prouver aussi. Mais, cette preuve ne fonctionne que pour un « fragment naturel » spécifique de dérivations. Les auteurs admettent qu'ils n'ont pas encore pleinement prouvé cela pour chaque cas étrange possible ; ils soupçonnent que cela est vrai de manière générale, mais cela reste une conjecture pour le système complet.
Il est Pratique : L'outil fonctionne dès maintenant. Il s'exécute dans un navigateur web, possède une extension VS Code, et a été utilisé dans des écoles d'été et des thèses de master.

Le « Résolveur de Formes »

L'une des parties les plus difficiles de ce math est de vérifier si une forme rentre dans une autre (par exemple, est-ce que ce triangle est à l'intérieur de ce carré ?). Rzk utilise un « solveur de topes » automatisé pour faire cela.

Comment ça marche : C'est un peu comme un détective essayant de résoudre un puzzle. Il examine les règles (topes) et essaie de voir si elles s'emboîtent.
Quelle est sa performance ? Dans des tests sur la bibliothèque sHoTT, le solveur a traité plus de 25 000 questions. La plupart ont été résolues instantanément (en une seule étape). Quelques-unes étaient très difficiles, prenant des milliers d'étapes, mais le solveur a réussi à les gérer.
La Limite : Le solveur est incomplet. C'est un prototype. Il fonctionne très bien pour les problèmes qu'il rencontre, mais les auteurs admettent qu'il pourrait manquer certaines solutions complexes car il ne cherche pas toutes les voies possibles. Ils prévoient de construire un solveur « parfait » à l'avenir, mais pour l'instant, le solveur actuel est « suffisant en pratique ».

Ce que Rzk Rejette

Le papier argumente explicitement contre l'idée qu'il soit nécessaire de prouver manuellement chaque petite inclusion de formes. Dans les systèmes plus anciens, vous deviez peut-être rédiger une longue preuve juste pour dire « ce triangle est à l'intérieur de ce carré ». Rzk rejette ce travail manuel ; il l'automatise.

Il rejette également l'idée des coercitions (ajouter des couches d'emballage supplémentaires pour faire entrer les choses). Les auteurs montrent que l'on peut avoir un système qui comprend les sous-types sans forcer l'ordinateur à insérer des étapes de conversion invisibles qui compliquent les mathématiques.

L'Essentiel

Rzk est un outil fonctionnel et utilisable qui amène la théorie abstraite des $\infty$ -catégories dirigées dans le monde réel des preuves vérifiées par ordinateur. Il divise les « boîtes magiques » mathématiques complexes en parties plus simples et transparentes, et prouve qu'il ne casse pas les anciennes règles tout en ajoutant de nouvelles capacités.

Les auteurs sont confiants que Rzk implémente fidèlement la théorie et que leur bibliothèque fonctionne. Ils sont certains que l'outil est utile pour l'enseignement et la recherche aujourd'hui. Cependant, ils sont moins certains des garanties théoriques complètes pour chaque cas limite possible (la conjecture de la conservativité totale) et admettent que leur solveur de formes est un prototype qui pourrait être amélioré. Ils n'ont pas résolu le problème de rendre le système terminable pour toutes les entrées possibles (la normalisation), ce qui reste un défi ouvert pour l'avenir.

En bref : Rzk est un moteur fonctionnel, vérifié et en pleine croissance pour un nouveau type de mathématiques, construit avec une conception fraîche qui facilite le travail de l'ordinateur sans perdre la magie de la théorie originale.

Énoncé du Problème
Le document traite de la nécessité d'un assistant de preuve capable de raisonner de manière synthétique sur les $\infty$ -catégories, spécifiquement les $(\infty, 1)$ -catégories. Bien que la Théorie des Types Homotopiques (HoTT) fournisse un cadre synthétique pour les $\infty$ -groupoïdes (où tous les morphismes sont inversibles), elle manque de l'appareil nécessaire pour gérer les morphismes dirigés, qui sont essentiels à la théorie des catégories. La Théorie des Types Simpliciaux (RSTT) de Riehl et Shulman a été proposée comme solution, introduisant des « formes » (comme des intervalles et des triangles dirigés) et des « types d'extension » pour définir les morphismes et les cellules supérieures de manière définitionnelle. Cependant, la RSTT reste largement un cadre théorique ; elle n'a pas été implémentée dans un assistant de preuve pratique. Les principaux défis de l'implémentation de la RSTT incluent le rendre le typage computationnelment faisable, la gestion des conditions de bord complexes des types d'extension, et la formalisation des hypothèses méta-théoriques (telles que les inclusions de formes) sur lesquelles les théorèmes de la RSTT reposent souvent de manière schématique.

Méthodologie
Les auteurs présentent Rzk, un assistant de preuve implémentant un raffinement computationnel de la RSTT. La méthodologie repose sur trois couches principales de développement :

Raffinement Théorique (Rzk Déclaratif) : Les auteurs définissent une variante déclarative de la RSTT (dRzk) qui introduit deux changements structurels clés pour rendre la théorie plus propice à une implémentation :
- Types d'Extension Scindés : Au lieu d'un seul formant de type d'extension, la dRzk sépare le concept en un type de fonction indexé par une forme (type $\Pi$ sur une forme) et une restriction de type (attachant une frontière définitionnelle à un type arbitraire). Cela permet au vérificateur de types de gérer des types intermédiaires où une fonction est appliquée mais où ses conditions de bord ne sont pas encore totalement résolues.
- Sous-typage sans Coercition : Pour gérer les identifications « silencieuses » souvent faites dans les preuves mathématiques (par exemple, traiter un type restreint comme son type sous-jacent), la dRzk introduit une relation de sous-typage explicite et sans coercition. Cela garantit que les termes restent inchangés lors des vérifications de sous-typage, évitant ainsi les problèmes de cohérence.
Formalisation Méta-Théorique : Les auteurs formalisent la « Couche de Paramètre Méta-Théorique » (MPL). Les théorèmes de la RSTT sont souvent énoncés schématiquement sur des cubes abstraits, des topes (formules logiques sur des cubes) et des familles de types. Rzk intègre ces éléments en tant que paramètres de premier rang au sein des définitions, permettant au système de gérer les inclusions de formes et les conditions latérales explicitement plutôt que comme des hypothèses implicites au niveau méta.
Implémentation Algorithmique : Les auteurs implémentent une version algorithmique (aRzk) comprenant :
- Typage Bidirectionnel : Un algorithme bidirectionnel standard adapté pour transporter le contexte de tope à travers tous les jugements.
- Calcul Dirigé par le Type : La normalisation est définie sur des termes élaborés qui mettent en cache leurs types, car la réduction dépend de l'information de type (spécifiquement, si un tope de frontière est vérifié).
- Solveur de Tope Automatisé : Un prototype de solveur pour la logique des formes (logique propositionnelle intuitionniste sur les intervalles dirigés) qui vérifie automatiquement les implications requises pour les inclusions de formes et les conditions de bord.
- Intégration du Sous-typage : Le sous-typage est intégré dans la vérification de l'égalité définitionnelle à l'aide d'un drapeau de variance, évitant l'insertion de coercitions explicites.

Contributions Clés

Assistant de Preuve Rzk : La première implémentation d'une théorie des types simpliciaux pour la théorie des $\infty$ -catégories synthétiques. Il est écrit en Haskell et fonctionne via un playground dans un navigateur et une extension VS Code.
Traduction Formelle et Conservativité : Le papier définit une traduction $\tau$ de la RSTT vers la dRzk et une rétro-traduction $\sigma$ . Ils prouvent que la traduction est fidèle (chaque preuve RSTT se traduit par une preuve Rzk) et conservative sur un fragment naturel de dérivations (la dRzk ne prouve rien de nouveau concernant les types RSTT). Ce fragment exige que les restrictions « autonomes » (restrictions qui ne sont pas attachées à un codomaine de type- $\Pi$ de forme) ne soient pas supposées comme hypothèses, mais seulement conclues.
Bibliothèque sHoTT : Les auteurs démontrent l'utilité de Rzk à travers la bibliothèque sHoTT, une bibliothèque standard contenant plus de 25 000 lignes de code et près de 1 500 déclarations. Cette bibliothèque formalise les concepts fondamentaux de la théorie des $(\infty, 1)$ -catégories synthétiques, incluant les types de Segal et de Rezk, les familles covariantes, les adjonctions, et la première formalisation du lemme de Yoneda $\infty$ -catégorique.
Détails d'Implémentation : Le papier détaille les algorithmes spécifiques pour la gestion de la logique des topes, le typage bidirectionnel avec contextes de tope, et l'intégration du sous-typage dans l'égalité définitionnelle.

Résultats

Correctitude : Le système vérifie avec succès la bibliothèque sHoTT. Les auteurs rapportent que le solveur de tope, bien qu'incomplet, traite la vaste majorité des requêtes de la bibliothèque efficacement (59 % en une seule étape, 99 % en moins de 35 étapes).
Corrections de Bugs : La comparaison rigoureuse entre la théorie déclarative et l'implémentation a révélé deux bugs de validité dans les versions précédentes (v0.7.7) liés à la comparaison de types d'identité et aux vérifications de sous-typage asymétriques, qui ont été corrigés dans la v0.7.8.
Performance : Le solveur représente environ 10 % du temps total de typage. Le système est capable de gérer des preuves complexes, telles que le lemme de Yoneda, sans intervention manuelle pour les inclusions de formes.

Signification et Revendications
Le papier affirme que Rzk est le premier et l'unique assistant de preuve pour la RSTT, comblant le fossé entre la proposition théorique de Riehl et Shulman et la formalisation pratique. Sa signification réside dans :

Permettre la Théorie des $\infty$ -Catégories Synthétiques : Il permet aux mathématiciens de raisonner sur les $(\infty, 1)$ -catégories directement dans la théorie des types, en utilisant les types d'extension pour définir les types de morphismes et la composition de manière définitionnelle, sans comptabilité propositionnelle.
Utilisabilité Pratique : L'existence de sHoTT démontre que la théorie n'est pas seulement théoriquement saine, mais aussi pratiquement utilisable pour des mathématiques non triviales.
Rigueur Théorique : En prouvant la fidélité et la conservativité, les auteurs garantissent que Rzk est une implémentation fidèle de la proposition originale de la RSTT, et non une variante divergente.

Les auteurs restent modestes quant aux problèmes ouverts. Ils reconnaissent que la conservativité totale pour toutes les dérivations dRzk (incluant celles avec des restrictions autonomes dans les hypothèses) est actuellement une conjecture. Ils notent également que la terminaison de la normalisation pour la RSTT n'est pas connue de manière générale, et que le solveur de tope est un prototype qui est sûr mais incomplet. Les travaux futurs incluent la mécanisation de la méta-théorie, l'implémentation d'un backend de normalisation par évaluation, et l'ajout du support pour les arguments implicites et les types inductifs supérieurs.

La Grande Idée : Une Nouvelle Façon de Construire

Ce que Rzk Peut Faire (et Ne Peut Pas Faire)

Le « Résolveur de Formes »

Ce que Rzk Rejette

L'Essentiel

Articles similaires