Natural number game(wwwf.imperial.ac.uk)
wwwf.imperial.ac.uk
Natural number game
https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/
14 comments
Did you use a similar tool to make this mixed formal/informal presentation of the squeeze theorem? https://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html
I used Patrick Massot's Lean Formatter https://github.com/leanprover-community/format_lean to make the Lean web page with the analysis theorem on, and Mohammad Pedramfar's Lean game maker was very much inspired by the code in the formatter.
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.
But if you just think of it as spaced repetition I'm sure everyone will agree that it's a great feature! :)
But if you just think of it as spaced repetition I'm sure everyone will agree that it's a great feature! :)
Note that the levels are "fake", so if you lost your progress that's sad, but you can just skip ahead to where you left. (We're looking into adding localStorage or something like that... but we aren't really coders. PRs are welcome!)
I'm having a lot of fun with this, having just completed addition.
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.
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: https://news.ycombinator.com/item?id=4014646
That's very polished, visually or at least typographically, which might not please everyone. But the idea of "proof by pointing" is solid.
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).
"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?]"
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.
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).
That's very polished, visually or at least typographically, which might not please everyone. But the idea of "proof by pointing" is solid.
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).
"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?]"
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.
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).
I totally agree that it's all over the place. I am a mathematician and have just thrown this together because I wanted my students to be able to learn Peano arithmetic (something I teach in my course) in a fun way. I am in desperate need of someone who knows something about UX.
Very cool! Didn't know about Lean (but I have some experience with Coq). Can't wait to dig in more. https://leanprover.github.io/about/
Note that https://leanprover.github.io is all about the frozen version of Lean 3, while the devs are working on Lean 4.
In the mean time, the community is maintaining a fork of Lean 3 with some nice features + lots of docs and other material. See https://leanprover-community.github.io/
Previously: A real nice similar project using Coq: https://news.ycombinator.com/item?id=4014646
That's very polished, visually or at least typographically, which might not please everyone. But the idea of "proof by pointing" is solid.
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).
"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?]"
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.
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).
That's very polished, visually or at least typographically, which might not please everyone. But the idea of "proof by pointing" is solid.
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).
"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?]"
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.
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 http://incredible.pm/
This is really fun. Thank you!
This is cool!
The natural number game was made by passing a repository which contains essentially nothing but Lean code, through this generic tool https://github.com/mpedramfar/Lean-game-maker 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 https://leanprover.zulipchat.com .