4 ms·

Possibly add the Incredible Proof Machine (https://incredible.pm https://incredible.pm)

082349872349872 3y ago
along these lines, the Natural Number Game ( https://adam.math.hhu.de/#/g/hhu-adam/NNG4 https://adam.math.hhu.de/#/g/hhu-adam/NNG4 ) (the ceiling on the game this is an installment of is pretty high, eg https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr... )
- thaumasiotes 3y ago
  Less math-focused, but same idea: https://nandgame.com https://nandgame.com
- thaumasiotes 3y ago
  incredible.pm is also a skin on a theorem prover. I had a lot more fun with incredible.pm; a lot of the difficulty in the Natural Number Game was in the UI being unclear. For example, I ran into a case where I had y <= d and I wanted y <= d + 1. The two relevant theorems here are the transitivity of the <= relation and the fact that n <= n+1 for all n. Both of those were in my "inventory". But I had no way to apply them. In incredible.pm, you'd have a block for "n <= n+1 for all n", you'd run that through a universal instantiator, and you'd get d <= d+1 as a result. Then you could use that as input to the transitivity theorem. But in the Natural Number game, where I had my hypothesis y <= d and my goal y <= d+1, there was no way that I was aware of to introduce the result d <= d+1, even though I had access to a theorem proving that specific fact. The solution turned out to be to say "apply le_trans" [to the goal y <= d+1], which gave me the intermediate goal y <= ?succ.inr.h.y . Hovering that upper bound then says "[This] Parses a synthetic hole [...] This syntax is used to construct named metavariables." Then, guessing something that might work but that the game certainly doesn't teach you to do, I closed that goal by calling "exact" on my hypothesis that said y <= d. This works† and unifies the value d with the named metavariable ?succ.inr.h.y . But I would not consider it a triumph of user experience. incredible.pm is also better in that it provides a playground where you can set up your own proofs of arbitrary theorems. † Well, the call to exact works. The call to apply le_trans split my goal "y <= d+1" into three goals, which were "y <= ?succ.inr.h.y , ?succ.inr.h.y <= d+1, and, for no reason I can imagine, ℕ. However, proving the first two goals completed the overall theorem, so I still don't know what it meant to have a third goal of "ℕ".
  - 082349872349872 3y ago
    I agree that incredible.pm is much better as a game; the NNG feels more like "as thin a veneer over Lean as they could get away with". Also, I was much less frustrated with the Lean 4 NNG because I'd already played "guess the verb" with the Lean 3 version, and I consulted the Lean docs at times; it's definitely not self-contained the way incredible.pm is. (that said, I liked NNG better because (a) the sequence felt more like actual theory* building than figuring a few cool puzzles, (b) I much prefer the textual input —even with the "guess the verb" problem— to clicking and dragging wires and blocks, and (c) I feel like I've learned something about how to use Lean, while it seems unlikely I'd be able to transfer much from the UX of incredible.pm — maybe if I'd tried 'modding' it I'd feel differently?) Maybe a fair way to put it is that the NNG is like ice hockey: for it to be fun at all you must first enjoy skating? * the old, Lean 3, NNG had as its crux "trichotomy for ℕ"; that was very satisfying to finally prove!
    - thaumasiotes 3y ago
      > (a) the sequence felt more like actual theory* building than figuring a few cool puzzles There is some of this in incredible.pm, and there's some of it in NNG. I made very little use of previous results in either one, except for a few levels of NNG that shame you for not generating simple proofs from immediately previous results. incredible.pm's "gameplay" element where you're challenged to prove the theorem in as few statements (blocks) as possible works against the idea of developing a bank of theorems and then applying those theorems to prove other theorems. I'm not so fond of it. > (b) I much prefer the textual input —even with the "guess the verb" problem— to clicking and dragging wires and blocks That's fair. The bigger issue I have is that in incredible.pm you're free to make statements if you think those statements will be useful to you, while NNG is very strict about making you work with only the statements you're given. In fact, there is one level in incredible.pm where I solved it in what was listed as the minimum number of blocks, but one of those blocks was a label. The label block is not doing any logical work, but sure enough, if I deleted the label block, incredible.pm was unable to unify the output that I had routed into the label block with the input that I had routed the label block into. So it would appear that at least one of the levels in incredible.pm specifically expects you to introduce your own statement with your own phrasing as an aid. > (c) I feel like I've learned something about how to use Lean, while it seems unlikely I'd be able to transfer much from the UX of incredible.pm I should be fair to NNG: I had extreme difficulty using existential statements correctly in incredible.pm, and more moderate difficulty managing to correctly use universal generalization. I think solving those levels gave me at least a decent mental model of how the theorem prover was handling quantifiers internally, and that should have transferred to a textual interface -- although it hasn't really stuck in my mind. > the old, Lean 3, NNG had as its crux "trichotomy for ℕ"; that was very satisfying to finally prove! That's still present in the current NNG. It is the proof I spent so much time complaining about above, the final level of Inequality World. (Or rather, that level wants you to prove that any two natural numbers are comparable, but you must use the trichotomy in order to do that, and you can't use what you haven't proved.) -------- I think NNG would benefit a lot from including more difficult proofs. (And from letting you introduce your own intermediate goals!) I was proud when I finished the proof that ∀x.(r(x)→⊥)→r(f(x)) ⟹ ∃x.r(x)∧r(f(f(x))) . I had to think about what the theorem was saying and write down a plan of attack. NNG doesn't really have anything like that. -------- Something I really did like in NNG was the remarks about (and eventual proof of) injectivity of the successor function. It's very interesting to me that the proof is based on, as NNG describes it, "the mathematically pathological pred[ecessor] function" - but only on cases where the pathology doesn't exist. (The proof involved introducing the function, making it inaccessible to the player, and instead giving the player the theorem "pred succ n = n", which is true without any exceptions.)
solardev 3y ago
So far the list only includes Steam games, but there have been many requests for older games, browser games, mobile games, etc. There is a discussion about it here: https://github.com/arcataroger/awesome-engineering-games/discussions/15 https://github.com/arcataroger/awesome-engineering-games/dis... Maybe there could be a sibling list that compiles all the non-Steam ones?

along these lines, the Natural Number Game ( https://adam.math.hhu.de/#/g/hhu-adam/NNG4 https://adam.math.hhu.de/#/g/hhu-adam/NNG4 ) (the ceiling on the game this is an installment of is pretty high, eg https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr... )

thaumasiotes 3y ago
Less math-focused, but same idea: https://nandgame.com https://nandgame.com
thaumasiotes 3y ago
incredible.pm is also a skin on a theorem prover. I had a lot more fun with incredible.pm; a lot of the difficulty in the Natural Number Game was in the UI being unclear. For example, I ran into a case where I had y <= d and I wanted y <= d + 1. The two relevant theorems here are the transitivity of the <= relation and the fact that n <= n+1 for all n. Both of those were in my "inventory". But I had no way to apply them. In incredible.pm, you'd have a block for "n <= n+1 for all n", you'd run that through a universal instantiator, and you'd get d <= d+1 as a result. Then you could use that as input to the transitivity theorem. But in the Natural Number game, where I had my hypothesis y <= d and my goal y <= d+1, there was no way that I was aware of to introduce the result d <= d+1, even though I had access to a theorem proving that specific fact. The solution turned out to be to say "apply le_trans" [to the goal y <= d+1], which gave me the intermediate goal y <= ?succ.inr.h.y . Hovering that upper bound then says "[This] Parses a synthetic hole [...] This syntax is used to construct named metavariables." Then, guessing something that might work but that the game certainly doesn't teach you to do, I closed that goal by calling "exact" on my hypothesis that said y <= d. This works† and unifies the value d with the named metavariable ?succ.inr.h.y . But I would not consider it a triumph of user experience. incredible.pm is also better in that it provides a playground where you can set up your own proofs of arbitrary theorems. † Well, the call to exact works. The call to apply le_trans split my goal "y <= d+1" into three goals, which were "y <= ?succ.inr.h.y , ?succ.inr.h.y <= d+1, and, for no reason I can imagine, ℕ. However, proving the first two goals completed the overall theorem, so I still don't know what it meant to have a third goal of "ℕ".
- 082349872349872 3y ago
  I agree that incredible.pm is much better as a game; the NNG feels more like "as thin a veneer over Lean as they could get away with". Also, I was much less frustrated with the Lean 4 NNG because I'd already played "guess the verb" with the Lean 3 version, and I consulted the Lean docs at times; it's definitely not self-contained the way incredible.pm is. (that said, I liked NNG better because (a) the sequence felt more like actual theory* building than figuring a few cool puzzles, (b) I much prefer the textual input —even with the "guess the verb" problem— to clicking and dragging wires and blocks, and (c) I feel like I've learned something about how to use Lean, while it seems unlikely I'd be able to transfer much from the UX of incredible.pm — maybe if I'd tried 'modding' it I'd feel differently?) Maybe a fair way to put it is that the NNG is like ice hockey: for it to be fun at all you must first enjoy skating? * the old, Lean 3, NNG had as its crux "trichotomy for ℕ"; that was very satisfying to finally prove!
  - thaumasiotes 3y ago
    > (a) the sequence felt more like actual theory* building than figuring a few cool puzzles There is some of this in incredible.pm, and there's some of it in NNG. I made very little use of previous results in either one, except for a few levels of NNG that shame you for not generating simple proofs from immediately previous results. incredible.pm's "gameplay" element where you're challenged to prove the theorem in as few statements (blocks) as possible works against the idea of developing a bank of theorems and then applying those theorems to prove other theorems. I'm not so fond of it. > (b) I much prefer the textual input —even with the "guess the verb" problem— to clicking and dragging wires and blocks That's fair. The bigger issue I have is that in incredible.pm you're free to make statements if you think those statements will be useful to you, while NNG is very strict about making you work with only the statements you're given. In fact, there is one level in incredible.pm where I solved it in what was listed as the minimum number of blocks, but one of those blocks was a label. The label block is not doing any logical work, but sure enough, if I deleted the label block, incredible.pm was unable to unify the output that I had routed into the label block with the input that I had routed the label block into. So it would appear that at least one of the levels in incredible.pm specifically expects you to introduce your own statement with your own phrasing as an aid. > (c) I feel like I've learned something about how to use Lean, while it seems unlikely I'd be able to transfer much from the UX of incredible.pm I should be fair to NNG: I had extreme difficulty using existential statements correctly in incredible.pm, and more moderate difficulty managing to correctly use universal generalization. I think solving those levels gave me at least a decent mental model of how the theorem prover was handling quantifiers internally, and that should have transferred to a textual interface -- although it hasn't really stuck in my mind. > the old, Lean 3, NNG had as its crux "trichotomy for ℕ"; that was very satisfying to finally prove! That's still present in the current NNG. It is the proof I spent so much time complaining about above, the final level of Inequality World. (Or rather, that level wants you to prove that any two natural numbers are comparable, but you must use the trichotomy in order to do that, and you can't use what you haven't proved.) -------- I think NNG would benefit a lot from including more difficult proofs. (And from letting you introduce your own intermediate goals!) I was proud when I finished the proof that ∀x.(r(x)→⊥)→r(f(x)) ⟹ ∃x.r(x)∧r(f(f(x))) . I had to think about what the theorem was saying and write down a plan of attack. NNG doesn't really have anything like that. -------- Something I really did like in NNG was the remarks about (and eventual proof of) injectivity of the successor function. It's very interesting to me that the proof is based on, as NNG describes it, "the mathematically pathological pred[ecessor] function" - but only on cases where the pathology doesn't exist. (The proof involved introducing the function, making it inaccessible to the player, and instead giving the player the theorem "pred succ n = n", which is true without any exceptions.)

solardev 3y ago

So far the list only includes Steam games, but there have been many requests for older games, browser games, mobile games, etc. There is a discussion about it here: https://github.com/arcataroger/awesome-engineering-games/discussions/15 https://github.com/arcataroger/awesome-engineering-games/dis... Maybe there could be a sibling list that compiles all the non-Steam ones?