Whilst providing a great language for checking the mathematical consistency and correctness of a result, Lean is great for something else too: corpus building. The proof of this is primarily in the projects Mathlib, Physlib, and CSLib, which form a corpus for these subjects.

They could have been written in human prose, but that is an unconstrained task, and it is hard to implement rules for scope, design, and generality, etc. Lean adds a mathematically natural constraint to this task, one that forces one to think carefully about design, scope, and generality. This constraint leads to a better corpus, one that, as a foundation, is very hard to argue with.