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

Overview & Synopsis

Lean 4 is under active development, and proofs that compile under one version may fail under later versions due to changes in the language, elaborator, libraries, or tooling. While the Lean community accepts this trade-off in exchange for rapid improvement, it creates challenges for long-term reproducibility of formalized mathematics and research artifacts. In this paper, we present xLaDe (eXperimental Lean 4 Advanced Development Ecosystem), a Lean 4 ecosystem framework designed to support reproducibility, preservation, and experimentation. xLaDe records toolchain metadata, dependencies, and execution context, enabling reconstruction of proof environments long after their original creation. The framework treats the Lean kernel as immutable infrastructure and wraps external Lean 4 projects without modifying their source code, allowing experiments to be conducted while preserving project integrity. xLaDe provides policy enforcement, experiment management, automated verification, and decentralized distribution mechanisms for Lean 4 projects. In this paper, we describe the design, implementation, security model, and experimental evaluation of xLaDe, and discuss its role as an ecosystem layer for improving the long-term sustainability of Lean 4 development and research.