Skip to content

add German translation - #162

Merged
kbuzzard merged 23 commits into
leanprover-community:mainfrom
Ljon4ik4:German_translation_added
Oct 5, 2026
Merged

kbuzzard merged 23 commits into
leanprover-community:mainfrom
Ljon4ik4:German_translation_added

Conversation

@Ljon4ik4

@Ljon4ik4 Ljon4ik4 commented Aug 6, 2026 •

Copy link
Copy Markdown
Contributor

This PR adds German language support.

Current breakages related to lean4game

The German translation uses the newer format with §-placeholders. This causes two problems rooted rather in lean4game than NNG4:

  • lean4game seems to change the key in the translation file if there is an escaped quote (\\" instead of \"), (it does not match lean-i18n), there is an issue Invalid escaping of translation strings lean4game#411

  • The other problem concern the infoview on the right, for some entries (rw rfl) the translations are not loaded. It can be fixed by changing in client/src/components/infoview/main.tsx, ExerciseStatement , ca. line 149
    (This is the line in the pinned version of lean4game, it probably would look different with the current one):

-          ... + t(data?.descrText, {ns: gameId})}
+          ... + gT(data?.descrText)}

I don't really know how to resolve this, it seems that there are two things to wait for:

  • The issues get fixed in lean4game
  • the corresponding lean4game version starts being used for NNG4

Notes:

  • The list of Theorems is sometimes called list of Lemmas, I added an explanation that Lemmas are 'small theorems' at one point in the German version (Also I indicated at one spot that 'Theorem' and 'Satz' are synonymous in German)
  • In Multiplication.L08addmul there seems to be a small error that 'addition distributes over multiplication' rather than vice-versa (the German matches the English, i.e. I did not fix it yet)
  • A few placeholders were translated manually (removing the placeholder), to fit German sentence structure.

AI use disclosure

An initial translated was created using claude OPUS, then I manually ran through all the entries and changed things which seemed strange and played through the full game to catch further errors.

@Ljon4ik4
Ljon4ik4 marked this pull request as draft August 6, 2026 06:45
@Ljon4ik4
Ljon4ik4 marked this pull request as ready for review August 8, 2026 22:48
@Ljon4ik4
Ljon4ik4 marked this pull request as draft August 9, 2026 11:42
@Ljon4ik4
Ljon4ik4 marked this pull request as ready for review August 9, 2026 20:23
@TentativeConvert

Copy link
Copy Markdown
Contributor

Vielen Dank! Ich habe großes Interesse an einer deutschen Übersetzung des NNG, bin aber gerade im Urlaub und kann mir das nicht genauer ansehen. Wahrscheinlich komme ich erst im September dazu.

@TentativeConvert

Copy link
Copy Markdown
Contributor

Die technischen Probleme sollten in der neuesten Version von lean-i18n behoben sein, aber der Update-Vorgang ist alles andere als einfach.

@TentativeConvert

Copy link
Copy Markdown
Contributor

Für den deutschen Titel wäre übrigens "Glasperlenspiel" mein erster, "Zahlenspiele" mein zweiter Favorit.

@Ljon4ik4

Ljon4ik4 commented Aug 9, 2026

Copy link
Copy Markdown
Contributor Author

Dankeschön, die Titel klingen sehr gut.
Ich glaube Zahlenspiele wäre dann mein Favorit.

Schönen Urlaub und bis September!

@TentativeConvert

Copy link
Copy Markdown
Contributor

@Ljon4ik4 Ich habe heute an der Übersetzung gearbeitet, aber ich habe hier keine Schreibrechte. Könntest Du mich zu Deinem Fork als Collaborator hinzufügen?

@Ljon4ik4

Ljon4ik4 commented Sep 9, 2026

Copy link
Copy Markdown
Contributor Author

@TentativeConvert
Ja, gerne, sollte erledigt sein. Sag Bescheid, wenn du mehr Rechte im benötigst, als per Default gegeben sind.

@TentativeConvert

Copy link
Copy Markdown
Contributor

I reviewed this today and made some changes. I would be very happy for this to be merged, assuming @Ljon4ik4 is also happy with my edits.

There are only a few points that might potentially be controversial:

  • The game is now called "Zahlenspiele" in the translation, not "Natürliches-Zahlen-Spiel", which I find too clunky.
  • The translation uses generic feminine throughout (Nutzerin, Mathematikerin, …).
  • I decided to pair "Ziel" (goal) with the verb "erreichen" rather than "lösen" or "schließen". This differs from the English original but feels more natural to me.

Some further conscious decisions are documented in the file Glossar-de.csv.

@Ljon4ik4

Ljon4ik4 commented Sep 9, 2026

Copy link
Copy Markdown
Contributor Author

Thanks a lot, I am very happy with the changes and improvements (especially with the controversial ones)!

@TentativeConvert

Copy link
Copy Markdown
Contributor

Commit f787b2e should be a small update after fixing the issues in the English source mentioned above. Unfortunately, it seems the line wrapping changed in the pot and po files, so the diff is very noisy and unusable.
Sorry about that.

@TentativeConvert

Copy link
Copy Markdown
Contributor

A preview of the game that includes this translation is now available at https://adam.math.hhu.de/#/g/tentativeconvert/nng4/.

@Ljon4ik4 Please give me a thumbs-up if/as soon as you're happy with this, then I'll ask the maintainers to merge.

@Ljon4ik4

Ljon4ik4 commented Oct 5, 2026

Copy link
Copy Markdown
Contributor Author

Thanks a lot, I am happy with it!
Only thing I would change still is adding your name to the translation credits.

@kbuzzard
kbuzzard merged commit 91dc0cf into leanprover-community:main Oct 5, 2026
1 check passed
@TentativeConvert

Copy link
Copy Markdown
Contributor

@Ljon4ik4 This is live now.

@Ljon4ik4

Ljon4ik4 commented Oct 6, 2026

Copy link
Copy Markdown
Contributor Author

Thanks a lot!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants