Comment by OrderlyTiamat

The lean proof being correct is easy to verify, whether it proves the thing we care about is much harder.

If your code compiles, are you sure it's bug free?