Zulip Chat Archive

Stream: lean4

Topic: nn game port


Matthew Ballard (Aug 04 2022 at 19:11):

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

Patrick Massot (Aug 04 2022 at 19:20):

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

Matthew Ballard (Aug 04 2022 at 19:20):

Ah I see. Thanks.

Kevin Buzzard (Aug 04 2022 at 20:32):

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 (Aug 04 2022 at 20:35):

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 (Aug 04 2022 at 20:40):

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 (Aug 04 2022 at 20:42):

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

Matthew Ballard (Aug 04 2022 at 20:43):

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

Matthew Ballard (Aug 04 2022 at 20:47):

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 (Aug 04 2022 at 20:50):

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 (Aug 04 2022 at 20:50):

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 (Aug 04 2022 at 20:58):

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

Alexander Bentkamp (Aug 05 2022 at 10:51):

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

Patrick Massot (Aug 05 2022 at 10:53):

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

Sebastian Ullrich (Aug 05 2022 at 11:00):

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 (Aug 05 2022 at 11:04):

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 (Aug 05 2022 at 11:06):

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 (Aug 05 2022 at 11:08):

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

Sebastian Ullrich (Aug 05 2022 at 11:12):

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

Patrick Massot (Aug 05 2022 at 11:13):

Oh, that's good to know.

Sebastian Ullrich (Aug 05 2022 at 11:14):

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 (Aug 05 2022 at 12:58):

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

Patrick Massot (Aug 05 2022 at 13:26):

Could you elaborate?

Matthew Ballard (Aug 05 2022 at 13:31):

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 (Aug 05 2022 at 15:02):

What problem is this meant to solve?

Matthew Ballard (Aug 05 2022 at 15:06):

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 (Aug 05 2022 at 15:09):

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


Last updated: Dec 20 2023 at 11:08 UTC