Not Letting Proofs Die: xLaDe, a Lean 4 Ecosystem Framework

Dans le monde des mathématiques modernes et du génie logiciel, il existe un mouvement croissant visant à écrire des preuves et des programmes d'une manière que les ordinateurs peuvent vérifier pour une exactitude absolue. Au lieu de compter sur l'œil humain pour repérer une erreur dans un argument complexe, les chercheurs utilisent des outils logiciels spécialisés appelés assistants de preuve. Ces programmes agissent comme des éditeurs rigoureux, vérifiant chaque étape logique pour s'assurer qu'un résultat est vrai au-delà de tout doute. Des systèmes comme Lean 4 sont devenus populaires pour ce travail, permettant à de grandes équipes de construire de vastes bibliothèques de mathématiques vérifiées et de logiciels sécurisés. Cependant, ces outils sont constamment mis à jour et améliorés. Tout comme une maison construite avec un ensemble de plans pourrait ne pas tenir debout si les règles de construction changeaient demain, une preuve mathématique qui fonctionne parfaitement aujourd'hui pourrait échouer à s'exécuter demain si la version du logiciel change. Cela crée un problème pour l'histoire à long terme de la science : si les outils évoluent trop rapidement, le travail accompli aujourd'hui pourrait devenir impossible à reproduire ou à comprendre dans le futur.

Une équipe de chercheurs de l'Université Centrale d'Andhra Pradesh a proposé une nouvelle façon de gérer ce défi, non pas en empêchant le logiciel de changer, mais en construisant une couche protectrice autour de lui. Ils appellent leur création xLaDe, qui signifie Experimental Lean 4 Advanced Development Ecosystem. Plutôt que d'essayer de figer le logiciel Lean dans le temps ou de le forcer à rester identique, xLaDe agit comme un système sophistiqué d'enregistrement et de gestion qui se situe au-dessus des outils existants. Son objectif est de traiter le logiciel de base comme un fondement solide et immuable tout en permettant aux chercheurs d'expérimenter librement à la surface, au-dessus de celui-ci. Le cadre est conçu pour capturer chaque détail de la manière dont une preuve a été exécutée — la version spécifique du logiciel utilisé, les dépendances et les conditions exactes de l'environnement — afin que le travail puisse être reconstruit des années plus tard, même si les outils sous-jacents ont évolué.

L'idée centrale de xLaDe est une séparation stricte entre le cœur de confiance du système et le travail expérimental qui s'opère autour de lui. Les chercheurs traitent le logiciel Lean lui-même comme une infrastructure immuable, ce qui signifie qu'il n'est jamais autorisé à être modifié par les expériences. Au lieu de cela, xLaDe fonctionne comme une couche d'orchestration, un ensemble d'outils qui enveloppe les projets externes sans toucher à leur code source. Cette approche permet aux scientifiques de tester de nouvelles idées, de changer de flux de travail et d'essayer différentes manières d'organiser leur travail sans risquer l'intégrité des preuves mathématiques elles-mêmes. Si une expérience échoue ou doit être abandonnée, elle peut être retirée proprement sans laisser de désordre ou affecter les parties stables du projet. Cette réversibilité est cruciale, car elle encourage les chercheurs à essayer de nouvelles choses sans craindre de briser définitivement leur travail.

Pour rendre ce système utilisable, l'équipe a construit un outil en ligne de commande qui sert d'interface principale pour les utilisateurs. Cet outil gère différents « modes » d'opération, permettant au même cadre de servir différents besoins. Il existe un mode d'intégration pour les débutants qui offre un guidage progressif, un mode expérimental où les chercheurs peuvent tester de nouveaux flux de travail et politiques, et un mode stable qui verrouille les choses pour une utilisation fiable à long terme. En mode stable, le système impose des règles strictes pour garantir que rien ne change de manière inattendue, ce qui le rend idéal pour préserver les résultats de la recherche. L'outil enregistre également automatiquement les métadonnées, telles que l'heure à laquelle une expérience a été exécutée et les versions spécifiques de logiciels impliquées, créant ainsi une piste d'audit détaillée. Cela garantit que toute personne examinant le travail dans le futur pourra voir exactement comment il a été réalisé et disposera des informations nécessaires pour le répéter.

Les chercheurs ont testé leur cadre avec deux expériences spécifiques pour voir s'il pouvait réellement fonctionner en pratique. Dans le premier test, ils ont pris un petit projet autonome créé spécifiquement pour l'étude et l'ont enveloppé dans le système xLaDe. Ils ont exécuté le processus de construction du projet via le cadre sans changer une seule ligne du code original. Le système a compilé les preuves avec succès et a enregistré les résultats, prouvant qu'il pouvait gérer des projets externes tout en les gardant complètement séparés du cadre lui-même. Dans un second test, plus rigoureux, ils ont appliqué la même méthode à un cours éducatif totalement indépendant sur Lean 4, créé par quelqu'un d'extérieur à leur équipe. Ce projet n'avait aucun lien préalable avec xLaDe. Le cadre a intégré le cours avec succès, a exécuté son processus de construction et a vérifié qu'il fonctionnait, le tout sans modifier les fichiers du cours ni le logiciel Lean. Ces résultats suggèrent que le système peut agir comme un enveloppe universelle, permettant à divers projets d'être gérés et reproduits selon un ensemble commun de règles.

La sécurité et la confiance sont centrales dans la conception de xLaDe. Les chercheurs reconnaissent qu'ils ne peuvent pas protéger contre toutes les menaces possibles, telles qu'un ordinateur compromis ou un initié malveillant ayant accès au code. Au lieu de cela, ils se concentrent sur la transparence et la vérification. Le système utilise plusieurs miroirs pour héberger le code, garantissant que si un site web tombe en panne, le projet reste accessible ailleurs. Il publie également des clés cryptographiques et des sommes de contrôle (checksums), qui sont des empreintes numériques permettant aux utilisateurs de vérifier que les fichiers qu'ils téléchargent sont exactement ceux que les auteurs avaient prévus, sans modifications cachées. Un élément clé de ce modèle de sécurité est la détection automatique de toute tentative de modification du logiciel Lean central. Si un script ou un utilisateur tente de changer le fondement immuable, le système détecte la violation et interrompt le processus, garantissant que l'intégrité des preuves mathématiques n'est jamais compromise par les outils expérimentaux.

L'article conclut que bien que xLaDe soit encore un projet expérimental et non une solution achevée, il offre une voie prometteuse pour l'avenir de la vérification formelle. Il ne prétend pas résoudre le problème de la rétrocompatibilité, où l'ancien code est forcé de fonctionner avec de nouveaux outils. Il propose plutôt une solution différente : préserver le contexte dans lequel le code a été écrit. En enregistrant l'environnement et en traitant les expériences comme des artefacts de recherche de premier rang, le cadre permet à la communauté de revisiter les résultats historiques avec confiance. Les auteurs soulignent que leur travail est une méthodologie pour mener la recherche sur les écosystèmes, fournissant une manière structurée de tester des idées, de documenter les échecs et de partager des outils réussis. À travers cette approche, ils espèrent créer un environnement durable où l'évolution rapide des assistants de preuve ne se fait pas au détriment de la perte du travail précieux construit sur eux.