After nine months of design, implementation, and orchestration, Lean's new module system I have been working on is now live in 4.26.0-rc1 and adopted throughout Mathlib. By introducing a system for checked and enforced API boundaries between files, it allows for changing proofs and other non-public information without any downstream rebuilds and drastically reduces the memory footprint of Mathlib imports to the lowest value ever since it was ported to Lean 4 two years ago.
