i’m finally learning to prove theorems (the earliest ones following from the Peano axioms) in lean, starting with the natural number game. it is actually somewhat fun, the same kind of fun that mtg has by being not too big to fully comprehend, but still engaging to solve.
(if you want to ‘play’ it as well, i suggest first reading a bit about what formal systems are and interpretation before starting. also, it was not clear to me at first when the game was introducing axioms vs derived theorems, so i wondered how some operations (e.g ‘induction’) were allowed, but it turned out that and some others are just in the list of Peano axioms.)
i’m finally learning to prove theorems (the earliest ones following from the Peano axioms) in lean, starting with the natural number game. it is actually somewhat fun, the same kind of fun that mtg has by being not too big to fully comprehend, but still engaging to solve.
(if you want to ‘play’ it as well, i suggest first reading a bit about what formal systems are and interpretation before starting. also, it was not clear to me at first when the game was introducing axioms vs derived theorems, so i wondered how some operations (e.g ‘induction’) were allowed, but it turned out that and some others are just in the list of Peano axioms.)
also, this reminded me of one of @Raemon’s idea (https://www.lesswrong.com/posts/PiPH4gkcMuvLALymK/exercise-solve-thinking-physics), ‘how to prove theorem’ feels like a pure case of ‘solving a problem that you (often) do not know how to solve’, which iiuc they’re a proponent of training on