German NNG

Stream: general

[Henrik Böving]

I spotted this PR on the natural number game the other day https://github.com/ImperialCollegeLondon/natural_number_game/pull/119 and am currently wondering, is it not being reviewed because none of the maintainers actually speak German so nobody really knows whether this is correct? Or is there an other reason to it?

[Yaël Dillies]

Oh unfortunately I think the Lean 3 NNG is soon to be outdated because we're about to switch to Lean 4.

[Henrik Böving]

That's also a thing I've been wondering^^ Everyone is talking about the mathlib switch to Lean 4 and that it will happen soon ish, is there some date or timeline for this somewhere?

[Yaël Dillies]

#lean4 is the place to look at

[Henrik Böving]

That's where I spend most of my time already yes :p but then I guess there isn't an actual timeline to it it's just soon ish.

[Julian Berman]

I think it's also possible @Kevin Buzzard hasn't seen the PR, he mentioned his GH notifications are off (because they're noisy) so you possibly can just wait for him to respond here and he may merge.

[Henrik Böving]

Oh it's not mine I just stumbled upon it by chance.

[Patrick Massot]

Kevin repeatedly explained he can't monitor this repo.

[Patrick Massot]

I suspect he'll happily merge this if some German speaking user he knows confirm this looks reasonable. Note this won't automatically deploy anywhere

[Kevin Buzzard]

Hi. Yes I'm afraid I completely ignore the repo. I figure that it works so why change it. What do you want me to do? I don't understand anything about the translation files. Thanks for pinging me here.

[Kevin Buzzard]

One reason I ignore it is that I know what I should be doing, I should be adding the lost levels (strong induction). But basically I'm waiting for Lean 4 and then someone will have to re-make the game maker.

[Henrik Böving]

Definitely sounds reasonable. I was just wondering^^

[Arthur Paulino]

I want to translate it to Brazilian portuguese too when it comes out for Lean 4