Ukraine is blееding again.
Today Russia attacked Ternopil. 19 people diеd. 66 іnjured. 16 of them are children.
Please don’t stay silent.
Tell the world .
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.