[readthenotes1]

I didn't like the clickbait title. I would have preferred something along the lines of

"Lean proves other program correct but not itself"