LEAN is exactly an expressive type system. Nothing more. The amazing thing is that the type system is so powerful that you can express cutting-edge mathematics with it and prove it correct.

In other words, proving something is essentially the same thing as type checking.

It absolutely blew my mind when I finally understood how it works. For that reason alone, LEAN is worth diving into. :)