First let me point out that you can jump to any level at any time, so you lose your progress, but only in a weak sense, if you lose your browser tab. You do lose your proofs though.<p>The natural number game was made by passing a repository which contains essentially nothing but Lean code, through this generic tool <a href="https://github.com/mpedramfar/Lean-game-maker" rel="nofollow">https://github.com/mpedramfar/Lean-game-maker</a> which makes the html pages from the Lean code. If there is anyone out there who understands the Lean game maker code (I don't, it was written by my co-author) and is interested in implementing some kind of client side storage then feel free to ping me either at my Imperial email address or at the Lean Zulip chat <a href="https://leanprover.zulipchat.com" rel="nofollow">https://leanprover.zulipchat.com</a> .
This is a very nice introduction to theorem proving, only caveat is that you cannot save your progress and the lean interpreter in the browser can lock up.<p>But if you just think of it as spaced repetition I'm sure everyone will agree that it's a great feature! :)
I'm having a lot of fun with this, having just completed addition.<p>I suppose it's natural [pun not intended] to feel like you don't really know what you're doing except symbolic expansion / replacement until you better grok the process, but perhaps that's part of the gamified fun.
Previously: A real nice similar project using Coq: <a href="https://news.ycombinator.com/item?id=4014646" rel="nofollow">https://news.ycombinator.com/item?id=4014646</a><p>That's very polished, visually or at least typographically, which might not please everyone. But the idea of "proof by pointing" is solid.<p>OTOH the 'UX' of this Lean system is all over the place: being told to remove the word 'sorry' is a bizarre way to start. With my browser and reasonable font sizes, it's just not possible to make the column wide enough to get all the text on the same page. So the following paragraph refers to something that's not visible (because it's at the end of the text).<p>"At the bottom of the text in this box, there's a lemma, which says that if x, y and z are natural numbers then xy + z = xy + z. Locate this lemma (if you can't see the lemma and these instructions at the same time, make this box wider by dragging the sides). Let's supply the proof. Click on the word sorry and then delete it. When the system finishes being busy, you'll be able to see your goal -- the objective of this level -- in the box on the top right. [NB if your system never finishes being busy, then your computer is not running the javascript Lean which powers everything behind the scenes. Try Chrome? Try not using private browsing?]"<p>This paragraph is also bad because it's all jumbled up. There's advice on resizing the UI, there's a casual/vague comment on browser compatibility, and there's the random placeholder word "sorry" which appears to have no pedagogical purpose. All this as well as the fact that the lemma isn't yet visible.<p>From a UX, accessibility, and teaching aspect, there's a lot of room for improvement. The current state of this app really comes across as idiosyncratic rather than straightforward. The experience has got a complicated, intrusive, handmade personality rather than being a lucid exposition. Logitext has a particular personality as well but it's a slicker one. It hides the incidental complexity better (though the implementation isn't necessarily as simple as it should be).
Very cool! Didn't know about Lean (but I have some experience with Coq). Can't wait to dig in more. <a href="https://leanprover.github.io/about/" rel="nofollow">https://leanprover.github.io/about/</a>
Previously: A real nice similar project using Coq: <a href="https://news.ycombinator.com/item?id=4014646" rel="nofollow">https://news.ycombinator.com/item?id=4014646</a><p>That's very polished, visually or at least typographically, which might not please everyone. But the idea of "proof by pointing" is solid.<p>OTOH the 'UX' of this Lean system is all over the place: being told to remove the word 'sorry' is a bizarre way to start. With my browser and reasonable font sizes, it's just not possible to make the column wide enough to get all the text on the same page. So the following paragraph refers to something that's not visible (because it's at the end of the text).<p>"At the bottom of the text in this box, there's a lemma, which says that if x, y and z are natural numbers then xy + z = xy + z. Locate this lemma (if you can't see the lemma and these instructions at the same time, make this box wider by dragging the sides). Let's supply the proof. Click on the word sorry and then delete it. When the system finishes being busy, you'll be able to see your goal -- the objective of this level -- in the box on the top right. [NB if your system never finishes being busy, then your computer is not running the javascript Lean which powers everything behind the scenes. Try Chrome? Try not using private browsing?]"<p>This paragraph is also bad because it's all jumbled up. There's advice on resizing the UI, there's a casual/vague comment on browser compatibility, and there's the random placeholder word "sorry" which appears to have no pedagogical purpose. All this as well as the fact that the lemma isn't yet visible.<p>From a UX, accessibility, and teaching aspect, there's a lot of room for improvement. The current state of this app really comes across as idiosyncratic rather than straightforward. The experience has got a complicated, intrusive, handmade personality rather than being a lucid exposition. Logitext has a particular personality as well but it's a slicker one. It hides the incidental complexity better (though the implementation isn't necessarily as simple as it should be).
Another kinda related website: The Incredible Proof Machine <a href="http://incredible.pm/" rel="nofollow">http://incredible.pm/</a>