I love that Lean completely destroys any suspicion of crackpottery.

There's a common trope of internet comments where you see people say they went off and did their own thing from first principles, pointedly avoiding existing work and preferring to follow their own ideas. And then you look at the thing and it's nigh invariably the disconnected ramblings of a person convinced of their own misunderstood genius.

But if the computer vouches for you, hard to avoid taking it seriously, that's the highest standard of rigor we have :)

(Nice proof by the way!)