euclid world boss level in need of Hints

[JadAbouHawili]

I would contribute hints but it would require having hints in German first then translating that.

the proof uses the have hypothesis : theorem := by ... syntax, but using have hypothesis : theorem syntax would accommodate having hints and guiding the user through sub-goals

[TentativeConvert]

Thanks for offering to contribute!

You don't actually need any German hints to begin with. This is an international project now :) What you need to is:

1. Add some rudimentary hints, preferably in English, to the lean file. Note that these hints need to be unique even after stripping all lean and latex snippets (everything in between `…`). You can add a random identifier to achieve this if necessary, like in this example:

   Robo/Game/Levels/Babylon/L03_sum_congr.lean

   Line 38 in 44275c9

   Hint "[Hint hwzk] Try `apply sum_congr`"

   Without the additional identifier [Hint hwzk], this line would reduce to the very generic Try §0, which appears all over the game.

2. lake build to create a new version of .i18n/template/Game.pot.

3. Open the English po-file at .i18n/en/Game.po in Poedit, choose Translation > Update From POT File from the menu, and load the file .i18n/template/Game.pot.

4. Add a fleshed-out version of your hint as an "English translation" of the rudimentary hint that you provided in the file.

However, please keep in mind that the idea of the game is to make the Boss levels solvable without hints. Everything needed to solve the Boss level should be explained in levels leading up to it. So if Euklid's Boss is too hard without hints, it probably means that some intermediate levels are missing.

What you could do is to add some hints of the form "yes, you're on the right track" and "if confused, go back to level X".

[TentativeConvert]

the proof uses the have hypothesis : theorem := by ... syntax …

I believe that syntax is used everywhere in the level lean files. It's just when you play the game in the browser that you don't need the := by syntax.