Comment by robinzfc

The title is quite misleading. This is a tutorial on reading a Lean verification script so the title should be like "Anatomy of a Lean verification script". As it is it suggests that all formal proofs look like this which they typically don't.