[LudwigNagasena]

I don’t understand the chess analogy. How is it in any way similar?

[kevinbuzzard]

Lean and the other theorem provers turn mathematical proofs into levels of a computer puzzle game, much like a chess puzzle.