Power World 10 uses ≠ which we don't yet know

[Ezra]

Power World 10 (Fermat's Last Theorem) is mostly pretty careful to frame it entirely in language we know: (a+1) instead of (n>0), etc. But it doesn't quite finish the job: it uses the symbol ≠, which we've never seen before unless we've digressed at least to Implication World 8. An unfamiliar symbol that we don't know how to manipulate, even a fairly common-sense one, undercuts the message that the tools we now have are enough to express big problems.

My current thought on how to improve this would be to

1. In the level explanation part of the text, mention that the symbol is new, but can for now be read in a common-sense way.
2. In the congratulations part of the text, along with the "go read Mathematics in Lean" suggestion, add an alternative of going to Implication World (if we haven't yet) to learn about ≠, and to work up to ≤ World where we'll have the full language to restate the problem more clearly.
3. (Future) If there's ever another world that depends on Power World and ≤ World, include in it a level showing how much more clearly we can now restate Fermat's Last Theorem.

Other strategies I've considered, but don't like as much, include

• Try to restate the theorem without ≠ (and without →).
• Try to explain Lean's symbol ≠ within the level text.
• Make this level depend on Implication World.

[joneugster]

I think the last option is the simplest one, i.e. add Dependency Implication → Power -- because of ≠ to the Game.lean file. @kbuzzard do you have any objection to adding this dependency to the tree?

[Tokarak]

It's not very good design if only the last level of the world depends on a previous world, especially if that level is purposefully unsolvable. Add a comment leading to Implication World instead.

[dalps]

I really don't see the point of this level, the Power world could very well do without it. Aside from being just math trivia, it's preventing the Power world from going all green in the main menu, which I find kind of upsetting. Why make it a level if it can't be solved?

[kbuzzard]

I think that the best solution to this is to move the FLT level to "hard world", a world which could come after "prime number world" (which also doesn't exist yet) and which could contain the twin prime conjecture, Goldbach conjecture, 3n+1 problem and FLT.

[costowell]

Hello! Any progress made on this? I'd be happy to submit a PR, but it sounds like there still needs to be more discussion.

Love the game and appreciative of all the hard work put in!

[SephQ]

I really don't see the point of this level, the Power world could very well do without it. Aside from being just math trivia, it's preventing the Power world from going all green in the main menu, which I find kind of upsetting. Why make it a level if it can't be solved?

What do you mean? I solved it with a truly remarkable proof using less than 300 lines of lean, but the GitHub comment limit is too small to contain it here. :'(

Edit: unfortunately, I have now died.

[dalps]

What do you mean? I solved it with a truly remarkable proof using less than 300 lines of lean, but the GitHub comment limit is too small to contain it here. :'(

You can always put it in a gist and link it here. I'm still curious :)