Zulip Chat Archive

Stream: new members

Topic: Is it time to update NNG to point to Lean 4 without redirect

Dan Abramov (Jul 27 2025 at 21:56):

Not sure who to ask about this, but this interstitial is kind of annoying.

Is there any harm in killing it and just doing the redirect right away?

Screenshot 2025-07-27 at 22.55.10.png

The Lean 4 version can always link to Lean 3 version if necessary.

Dan Abramov (Jul 27 2025 at 21:57):

@Kevin Buzzard I think this one is a question to you

Kevin Buzzard (Jul 28 2025 at 12:43):

I totally agree that it's really annoying (I find NNG by googling and I always get to this annoying page) and probably have edit access to that page but I'll have to ask someone how to get to it and even when I do get to it I have no real clue what to change it to. IIRC I asked here a couple of years ago and someone just literally posted some HTML code which I just cut and pasted.

Update: I've asked a local server person to make it a redirect.

Dan Abramov (Jul 28 2025 at 13:27):

Thanks!

This should work fine for doing it from the HTML:

<!DOCTYPE html>
<html>
<head>
  <meta http-equiv="refresh" content="0; url=https://adam.math.hhu.de">
</head>
</html>

Or if it can be done on the server, even better.

Kevin Buzzard (Jul 28 2025 at 17:11):

Someone else has done it for me. I had to click reload because of cache issues but now it jumps directly to the Lean 4 game.

Last updated: Dec 20 2025 at 21:32 UTC