I didn't like the clickbait title. I would have preferred something along the lines of"Lean proves other program correct but not itself"