Claude can generate Lean code all day long, but eventually you have to read the code and more importantly, the theorems verifying the software's correctness properties. Learn how to read Lean theorems in this short guide.