(Asking as an interested noob) -- How is this different to something like 'assert' statements in Python?

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.

It works on the type system level instead of at runtime. So you don't actually need to "run" any code to verify it, and you can verify it for all possible inputs, even infinity of them, rather than for the ones that exist in your test.

Assertions are for testing at runtime. They demonstrate that the behavior is correct on one input when it runs. Formal verification proves that the code is correct on _all_ inputs _before_ it runs.

it's like proof by induction versus trying every number from 0 to infinity