## Stream: lean4

### Topic: Port NNG to Lean 4

#### Huỳnh Trần Khanh (Jan 28 2021 at 14:14):

Is it possible to port NNG to Lean 4? Will we do it?

#### Kevin Buzzard (Jan 28 2021 at 14:19):

I would imagine that porting the Lean code would be a very pleasant exercise, and indeed a few weeks ago someone posted to this Zulip a bunch of NNG stuff in Lean 4. I have no clue about how one turns Lean 4 code into a browser game though so cannot comment on that. It would probably be not unfair to say that this is not high priority for me right now (although of course if someone else wants to take it on I'm not going to be complaining!). However once we're at the stage where we are expecting newcomers to use Lean 4 rather than Lean 3 (and I have no clue about when this will happen, I am adopting a "wait and see" approach here because I have no idea about any of the subtleties involved) then I would imagine that this would become a much higher priority, because NNG seems to work as a way of attracting people with a mathematical interest to Lean.

#### Sebastian Ullrich (Jan 28 2021 at 14:24):

step 1: figure out how to compile Lean 4 to Wasm
step 2: figure out how to connect the Lean 4 server with a web editor
step 3: remove "and don't forget the comma"

#### Kevin Buzzard (Jan 28 2021 at 14:25):

you forgot all semicolons in your message

#### Reid Barton (Jan 28 2021 at 14:25):

I noticed rw doesn't like to apply refl rfl afterwards now, so Kevin will be happy about that!

#### Sebastian Ullrich (Jan 28 2021 at 14:26):

Kevin Buzzard said:

you forgot all semicolons in your message

I prefer whitespace sensitivity

#### Kevin Buzzard (Jan 28 2021 at 14:26):

So we see!

Last updated: May 18 2021 at 22:15 UTC