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

In de wereld van de moderne wiskunde en software engineering is er een groeiende beweging om bewijzen en programma's op een manier te schrijven die computers kan controleren op absolute correctheid. In plaats van te vertrouwen op menselijke ogen om een fout in een complex argument op te sporen, gebruiken onderzoekers gespecialiseerde softwaretools die bewijsassistenten worden genoemd. Deze programma's fungeren als rigoureuze redacteuren die elke logische stap verifiëren om te garanderen dat een resultaat zonder enig twijfel waar is. Systemen zoals Lean 4 zijn populair geworden voor dit werk, waardoor grote teams enorme bibliotheken van geverifieerde wiskunde en beveiligde software kunnen opbouwen. Deze tools worden echter constant bijgewerkt en verbeterd. Net zoals een huis dat gebouwd is met één set blauwdrukken misschien niet overeind blijft als de regels voor constructie morgen veranderen, kan een wiskundig bewijs dat vandaag perfect werkt, morgen niet meer draaien als de softwareversie verandert. Dit creëert een probleem voor de lange termijn van de wetenschappelijke geschiedenis: als de tools te snel evolueren, zou het werk van vandaag in de toekomst onmogelijk te reproduceren of te begrijpen kunnen zijn.

Een team van onderzoekers van de Central University of Andhra Pradesh heeft een nieuwe manier voorgesteld om dit probleem aan te pakken, niet door de software te stoppen met veranderen, maar door een beschermende laag eromheen te bouwen. Ze noemen hun creatie xLaDe, wat staat voor de Experimental Lean 4 Advanced Development Ecosystem. In plaats van te proberen de Lean-software in de tijd te bevriezen of te dwingen hetzelfde te blijven, fungeert xLaDe als een geavanceerd registratie- en beheersysteem dat bovenop de bestaande tools zit. Het doel is om de kernsoftware te behandelen als een solide, onveranderlijke fundering, terwijl onderzoekers vrij kunnen experimenteren op het oppervlak daarboven. Het framework is ontworpen om elk detail vast te leggen van hoe een bewijs werd uitgevoerd—de specifieke versie van de software die werd gebruikt, de afhankelijkheden en de exacte condities van de omgeving—zodat het werk jaren later kan worden gereconstrueerd, zelfs als de onderliggende tools inmiddels verder zijn gegaan.

Het kernidee achter xLaDe is een strikte scheiding tussen het vertrouwde hart van het systeem en het experimentele werk dat eromheen plaatsvindt. De onderzoekers behandelen de Lean-software zelf als immutabele infrastructuur, wat betekent dat deze nooit toegestaan is om door de experimenten te worden gewijzigd. In plaats daarvan werkt xLaDe als een orchestratielaag, een set tools die rond externe projecten heen werkt zonder hun broncode aan te raken. Deze aanpak stelt wetenschappers in staat om nieuwe ideeën te testen, workflows te veranderen en verschillende manieren uit te proberen om hun werk te organiseren, zonder de integriteit van de wiskundige bewijzen zelf in gevaar te brengen. Als een experiment fout gaat of moet worden weggegooid, kan het schoon worden verwijderd zonder een rommel achter te laten of de stabiele delen van het project te beïnvloeden. Deze omkeerbaarheid is cruciaal, omdat het onderzoekers aanmoedigt om nieuwe dingen te proberen zonder de angst hun werk permanent te beschadigen.

Om dit systeem bruikbaar te maken, heeft het team een command-line tool gebouwd die fungeert als de belangrijkste interface voor gebruikers. Deze tool beheert verschillende "modi" van operatie, waardoor hetzelfde framework aan verschillende behoeften kan dienen. Er is een onboarding-modus voor beginners die milde begeleiding biedt, een experimentele modus waar onderzoekers nieuwe workflows en beleid kunnen testen, en een stabiele modus die de boel vergrendelt voor betrouwbaar, langdurig gebruik. In de stabiele modus handhaaft het systeem strikte regels om ervoor te zorgen dat er niets onverwacht verandert, wat het ideaal maakt voor het bewaren van onderzoeksresultaten. De tool registreert ook automatisch metadata, zoals de tijd waarop een experiment werd uitgevoerd en de specifieke softwareversies die betrokken waren, waardoor een gedetailleerd auditspoor wordt gecreëerd. Dit zorgt ervoor dat iedereen die het werk in de toekomst bekijkt, precies kan zien hoe het is gedaan en over de informatie beschikt die nodig is om het te herhalen.

De onderzoekers testten hun framework met twee specifieke experimenten om te zien of het in de praktijk echt kon werken. In de eerste test namen ze een klein, zelfstandig project dat specifiek voor de studie was gemaakt en plaatsten dit binnen het xLaDe-systeem. Ze draaiden het build-proces van het project door het framework zonder een enkele regel van de originele code te wijzigen. Het systeem compileerde de bewijzen succesvol en legde de resultaten vast, wat bewees dat het externe projecten kan beheren terwijl het ze volledig gescheiden houdt van het framework zelf. In een tweede, strengere test pasten ze dezelfde methode toe op een volledig onafhankelijke educatieve cursus over Lean 4, gemaakt door iemand buiten hun team. Dit project had geen eerdere relatie met xLaDe. Het framework integreerde de cursus succesvol, draaide het build-proces en verifieerde dat het werkte, zonder de cursusbestanden of de Lean-software te wijzigen. Deze resultaten suggeries dat het systeem kan fungeren als een universele wrapper, waardoor diverse projecten onder een gemeenschappelijke set regels kunnen worden beheerd en gereproduceerd.

Beveiliging en vertrouwen staan centraal in het ontwerp van xLaDe. De onderzoekers erkennen dat ze niet tegen elke mogelijke dreiging kunnen beschermen, zoals een gecompromitteerde computer of een kwaadwillende insider met toegang tot de code. In plaats daarvan richten ze zich op transparantie en verificatie. Het systeem gebruikt meerdere spiegels (mirrors) om de code te hosten, wat ervoor zorgt dat als een website offline gaat, het project elders toegankelijk blijft. Het publiceert ook cryptografische sleutels en checksums, wat digitale vingerafdrukken zijn waarmee gebruikers kunnen verifiëren dat de bestanden die ze downloaden exact zijn wat de auteurs bedoelden, zonder verborgen wijzigingen. Een essentieel onderdeel van dit beveiligingsmodel is de automatische detectie van elk poging om de kern-Lean-software te wijzigen. Als een script of een gebruiker probeert de onveranderlijke fundering te wijzigen, detecteert het systeem de overtreding en stopt het proces, zodat de integriteit van de wiskundige bewijzen nooit in gevaar komt door experimentele tools.

Het artikel concludeert dat hoewel xLaDe nog een experimenteel project is en geen voltooide oplossing, het een veelbelovend pad biedt voor de toekomst van formele verificatie. Het claimt niet het probleem van backward compatibiliteit op te lossen, waarbij oude code gedwongen wordt om met nieuwe tools te werken. In plaats daarvan biedt het een andere oplossing: het bewaren van de context waarin de code is geschreven. Door de omgeving vast te leggen en experimenten te behandelen als eersteklas onderzoeksartefacten, stelt het framework de gemeenschap in staat om historische resultaten met vertrouwen te herzien. De auteurs benadrukken dat hun werk een methodologie is voor het uitvoeren van ecosysteemonderzoek, wat een gestructureerde manier biedt om ideeën te testen, fouten te documenteren en succesvolle tools te delen. Door deze aanpak hopen ze een duurzame omgeving te creëren waarin de snelle evolutie van bewijsassistenten niet ten koste gaat van het waardevolle werk dat erop gebouwd is.