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

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. :)