search

Trequetrum / lean4game-logic

Make/Encode some basic logic puzzles
MIT License
1 stars 3 forks source link

Level 5 / 7 : Rewriting on the final world (World: Redux: ↔ World Tactics) on "A Lean Intro to Logic" and general feedback #7

Open joneugster opened 1 month ago

joneugster commented 1 month ago

A report by @awefhio originally posted at leanprover-community/lean4game#232.

I got stuck on Level 5 / 7 : Rewriting on the final world (World: Redux: ↔ World Tactics).

image

Can't think of anything to use "apply" on , and no alternative ideas due to limited tactics. I admit I might be missing something very obvious but it's out of my reach, although I'd still like to check whether it's a problem with the level.

Overall speaking, I feel like the logic game is much less polished than the natural number game and the set theory game (which I both completed). Particularly compared to the set theory game, many similar theorems have inconsistent names (e.g. And.intro vs and_intro).

The instructions also is confusing at times, I don't find the analogies particularly helpful, but I can understand if they're aimed at a less experienced audience, yet the levels themselves seem to assume a familiarity with lambda calculus. I think it'll be much more helpful if the learning curve on lambda notation can be smoothed out.

Trequetrum commented 1 month ago

This brings up some points that have been on my mind for a while.

1: The play testers I watched play this game never played the Natural Numbers or Set Theory Game. Early on, I saw it helped play testers when I remove the way Lean does namespace resolution so we're never in the situation where some theorems are separated by dots and some by underscores. I'm not sure if this is the best choice in the long run as people who are familiar with Mathlib/Natutal Number Game/Set Theory Game may come in with other expectations.

2: The flavor text isn't really helpful in finding a solution. It can give context around the logical operators (though even this can be tenuous), which helps a bit with players who have never done any formal logic. It's sort of how intro to logic textbooks do it, right? Even so, you have to learn to write terms as evidence and the flavor text isn't helpful there. I think the flavor text can more or less stand on its own merits, though to do so convincingly it could use some improvements. It would probably also help to have some way to signal which text is there for fun and which is meant to be instructive.

3: The level you got stuck on is way too long. It doesn't require any steps/tricks a player wouldn't have seen on earlier levels. I've seen play-testers who have had zero exposure to Lean other than Intro to Logic complete the level. So it's not broken, but it's not good either. Rather than feeling accomplished when you make it to the end, I can imagine you may well just feel tired. I've been toying with the idea of removing the redux worlds.

I think it'll be much more helpful if the learning curve on lambda notation can be smoothed out.

I'll think about this. My experience with play-testers has been that they get to the right expression without having any idea that they're sort of doing lambda calculus. They think about the lambda terms directly as evidence for the propositions (with no regard for the runtime behavior of functions calls or anything like that). In many ways, I guess it's a static, non-computational view of what's happening.

I don't know if that's a good or a bad thing. Certainly it can get you through the logic game, but it feels pretty limiting. Getting the right balance here is certainly something worth spending some more effort on.