Hacker News Reader

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

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