nullenvk@kbin.social to Mathematics@kbin.social · edit-21 year agoThe Natural Number Gamewww.ma.imperial.ac.ukexternal-linkmessage-square1fedilinkarrow-up17file-text
arrow-up17external-linkThe Natural Number Gamewww.ma.imperial.ac.uknullenvk@kbin.social to Mathematics@kbin.social · edit-21 year agomessage-square1fedilinkfile-text
An interactive introduction to the Lean theorem prover and “a part-book part-game which shows the power of induction”.
minus-squareObject@kbin.sociallinkfedilinkarrow-up1·1 year agoI don’t know if it is hosted somewhere, but there’s already a (not completed) Lean4 version: https://github.com/PatrickMassot/NNG4
I don’t know if it is hosted somewhere, but there’s already a (not completed) Lean4 version: https://github.com/PatrickMassot/NNG4