nn game port

Stream: lean4

[Matthew Ballard]

Is there a port of the Natural Number Game to Lean 4?

[Patrick Massot]

This cannot exist as a website because Lean 4 doesn't run in a browser.

[Matthew Ballard]

Ah I see. Thanks.

[Kevin Buzzard]

Leo was encouraging me to switch to Lean 4 for my UG intro to proof course, but part of the course is on natural numbers and I wrote NNG to teach it to them, so right now if I switched I'd have some hybrid course which was partially in Lean 3 and partially in Lean 4 :-(

[Matthew Ballard]

This is exactly my use case. In my course, I offered NNG as an option for a final project. It was overwhelmingly popular. Given that tactic-based proofs are optional, the 3/4 dichotomy is a bit more forgivable.

[Henrik Böving]

I don't think teaching Lean without tactics is a good idea though really, its a fundamental part of the way Lean operates different from e.g. the likes of Agda

[Matthew Ballard]

I wouldn't say the goal of the course is teaching Lean. It is teaching rigorous thought and care.

[Matthew Ballard]

I agree that, at this level, you can more easily swap another language.

[Matthew Ballard]

For this course, Lean supercharges the formative assessment feedback loop allowing for more cycles than is generally possible in a purely human-assessed course.

[Matthew Ballard]

It also presents the core concepts from a different perspective. In general, more ways of saying something translates into better overall student comprehension.

[Matthew Ballard]

It also presents the core concepts from a different perspective. In general, more ways of saying something translates into better overall student comprehension.

[Patrick Massot]

Note that building a NNG as a standalone application using Lean 4 is totally doable, but students would need to download it.

[Alexander Bentkamp]

Another option would be to run Lean on a server instead the client.

[Patrick Massot]

Yes. I wonder whether this would be horribly slow or not.

[Sebastian Ullrich]

Have you tried Gitpod with either Lean 3 or 4 before? It's perfectly usable. As long as the server has enough resources for all the concurrent connections of course, in the case of a custom VS Code server.

[Patrick Massot]

I tried GitPod but in the nng context the authentication barrier is really bad, and you don't get the custom user interface.

[Sebastian Ullrich]

Makes sense, but my point was that if Gitpod is fast enough, there's no reason a custom server-side solution should be any slower

[Patrick Massot]

On gitpod the editor and lean run on the same server, right?

[Sebastian Ullrich]

No, the editor runs in your browser, the Lean process on the Gitpod server

[Patrick Massot]

Oh, that's good to know.

[Sebastian Ullrich]

It's the same protocol as VS Code's "Remote Development" I think, where you can connect your local VS Code to Lean in a container or on a different machine via SSH

[Matthew Ballard]

Another method for authentication occurred to me: Tailscale. Anyone on your tailnet can then access it normally.

[Patrick Massot]

Could you elaborate?

[Matthew Ballard]

Tailscale lets you easily create a "personal" VPN and assigns static IPs to all devices on that network. If you stand up a server on one, then anyone else can access it via the IP in the browser.

[Patrick Massot]

What problem is this meant to solve?

[Matthew Ballard]

If you need to restrict access to a server, say if you set up a server-based version of VS Code with Lean on the same machine.

[Patrick Massot]

I see. It doesn't solve the GitPod issue but a potential more sophisticated setup issue.