I’m an noob to Lean myself, but my best explanation is that asserts are checks that happen at runtime. Imagine compile-time asserts, where the compiler is able to determine the validity of assertions without needing to run the program. Formal verification techniques make this possible. In Lean, it is possible to write a proof that, if true, guarantees that the code works.