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.

Our experiments with Lean and formal verification continue to bear fruit. To further our knowhow and experience, we set out to see if we could apply Lean's strengths to a more advanced topic: compiler optimizations. Traditional verified compilers focus on semantic preservation of already-written C code, limiting their