No mizar no proof

Lean is the Mizar here. For those who have no clue what this is about, Mizar [1] was an early automated theorem prover. Can't wait for HN to add AI features to explain concepts in the sideline, and autovoting.

[1] https://en.wikipedia.org/wiki/Mizar_system