Jonathan Blow playing NNG on Twitch

Stream: general

[Bulhwi Cha]

Basic stuff just fails all the time.

This is a bad puzzle because the obstruction is completely uninteresting.

I'll try to complete Level 8 of NNG's Tutorial World, which is about proving 2 + 2 = 4.

[Bulhwi Cha]

example : (2 : ℕ) + 2 = 4 := by
  nth_rewrite 2 [two_eq_succ_one]
  rw [add_succ]
  rw [← succ_eq_add_one]
  rw [← three_eq_succ_two]
  rw [← four_eq_succ_three]
  rfl

[Bulhwi Cha]

Perhaps programmers like him would like to try other Lean tutorials instead.

[Bulhwi Cha]

They need to know the inductive definition of the natural numbers in Lean.

[Bhavik Mehta]

I disagree that needs to be a prerequisite, since this is introduced and explained in level 3 of the tutorial world

[Bulhwi Cha]

From https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Tutorial/level/3:

• 0 is a number.
• If n is a number, then the successor succ n of n is a number.

[Bulhwi Cha]

Bulhwi Cha said:

They need to know the inductive definition of the natural numbers in Lean.

Oh, I think I should've said as follows:

They need to know the inductive definition of the addition of two natural numbers in Lean.

[Bhavik Mehta]

That's explained in levels 5 and 7 of the tutorial

[Bulhwi Cha]

Hmm, you're right. Then, all I can say is that they might need more examples.

[Bulhwi Cha]

Something like 2 + 1 = 3; it'd be easier to prove than 2 + 2 = 4. They might also need more time to get used to the fact that succ n is the same as n + 1.

[Bolton Bailey]

It's interesting that his instinct is that add_assoc requires two uses of induction.

[Bolton Bailey]

You could just make an interesting video game where you're clicking on the strats

Relevant to @Jovan Gerbscheid 's Lean Together talk!

[Bhavik Mehta]

Bolton Bailey said:

It's interesting that his instinct is that add_assoc requires two uses of induction.

And similarly that add_right_comm and zero_mul require induction at all. I think all of these are because of the usual puzzle-game-instinct that after you learn a new technique, the next few levels develop that technique specifically

[Snir Broshi]

Progress so far:

image.png

[Snir Broshi]

This crossover is crazy, I wonder if it's because of interest in PL (which is obvious as the creator of Jai) or rather interest in ITPs

[David Michael Roberts]

Bulhwi Cha said:

Jonathan Blow is learning Lean right now: https://www.twitch.tv/j_blow.

Ah, he didn't keep the VOD on Twitch. A pity!

[Johan Commelin]

A pity indeed! I think there would be a wealth of valuable feedback on Lean UX and improving the Lean game experience!

Maybe someone should reach out, and ask him if he has a copy that he wants to share? @ the people that watched the stream: do you have recollections of feedback / insights that he gave?

[Notification Bot]

17 messages were moved here from #general > Lean in the wild by Johan Commelin.

[Bolton Bailey]

My best recollection of points of friction:

• He spent at least a minute at one point trying to get dark mode to work
• He was frustrated by lag, and thought it would be a better experience for it to run locally (but I think he also seemed to appreciate that that would be technically difficult to achieve)
• At one point he needed to apply add_comm at two different places in the goal, so of course he tried repeat rw [add_comm] and rw [add_comm, add_comm], If you understand Lean well, you see why this is mistaken, but you can see why a beginner would feel like these might work.
• I already mentioned the induction, and the desire for a point and click UI.

[Chris Bailey]

Johan Commelin said:

A pity indeed! I think there would be a wealth of valuable feedback on Lean UX and improving the Lean game experience!

Maybe someone should reach out, and ask him if he has a copy that he wants to share? @ the people that watched the stream: do you have recollections of feedback / insights that he gave?

A big one throughout the stream was frustration with the pretty printer omitting parentheses; succ a + b is not clear about whether it's succ (a + b) or (succ a) + b, which ends up being a big deal when you have a very limited and strict toolkit of lemmas to rewrite with. NNG does not use the dot notation either (e.g. a.succ).

The error message when you try to rewrite with a lemma that needs an additional argument to figure out what it's supposed to do is not good, something about one of the arguments being a metavariable. Chat had to explain that one sometimes needs to write rw [mul_one a] instead of just rw [mul_one]. IIRC he was using the wrong lemma to begin with, but he didn't get "instance of the pattern couldn't be found" either.

Why is the "rewrite" tactic written "rw" (abbreviated), but the "nth rewrite" tactic is written out "nth_rewrite" (with no abbreviation).

There was a surprising amount of consternation about the term "goal" not being explained, which came about because he was not clear on why the supposed goal was changing with the rewrites. Chat attempted to explain backward vs. forward reasoning in this context and eventually talked him off the ledge on that, I think. My own experience of watching people play NNG has consistently made me think that have should be one of the tools available to players, which may have been useful in this case.

Some general frustration with the implications of NNG being a web application, amplified by jonathan blow being jonathan blow, but overall he seemed to have a pretty good time. There were a couple of "we're probably going to stop after one or two more levels"s that he ended up blowing past, which is usually a positive sign.

[Johan Commelin]

Maybe NNG should just print all parentheses by default? It already deviates from some other Lean defaults.

[Chris Bailey]

If dot notation is out of the question, then that's not a bad idea. I don't recall there being anything too crazy that will lisp-out at them.

[Patrick Massot]

Can anyone provide some context by explaining who is this Jonathan Blow?

[Sébastien Gouëzel]

Very famous video games designer, thinking deeply about game mechanism, and thinking very highly of himself.

[Snir Broshi]

Also created a programming language (Jai) with the intent to replace C++, so has interest in programming languages

[Aaron Liu]

Chris Bailey said:

The error message when you try to rewrite with a lemma that needs an additional argument to figure out what it's supposed to do is not good, something about one of the arguments being a metavariable. Chat had to explain that one sometimes needs to write rw [mul_one a] instead of just rw [mul_one].

iirc it was ← mul_one which rewrites ?m into ?m * 1

[James E Hanson]

Bolton Bailey said:

• He was frustrated by lag, and thought it would be a better experience for it to run locally (but I think he also seemed to appreciate that that would be technically difficult to achieve)

I have wondered about this before. I'm under the impression that NNG only needs a fairly small fragment of Lean which in particular doesn't involve much type class inference. I'm also under the impression that the biggest factor in the elaborator's performance is type class inference. So what is the barrier to running it locally?

[Aaron Liu]

I don't think it's typeclass inference

[Aaron Liu]

hmm I actually don't know what are the performance of the various things on the elaborator

[Ruben Van de Velde]

It would be interesting to profile, but I'm not sure the lag is caused by pure lean rather than the client-server set up

[Aaron Liu]

sometimes the server freezes and it takes absurdly long for it to start working again

[Miyahara Kō]

Patrick Massot said:

Can anyone provide some context by explaining who is this Jonathan Blow?

The creator of "Braid" and "The Witness".

[Arthur Paulino]

Basic stuff just fails all the time.

This frustration is expected. Anyone who's minimally trained in math can perform symbolic manipulations pretty quickly, just using the mind. But in Lean, without tactics that can capture the way people usually think, it can feel underwhelming.

Unless people have at least some undergrad experience with math (I'm talking about a math undergrad course, not some applied math for engineering) and/or deeper interest in learning Lean, it's very likely to feel underwhelmed with the most basic manipulations in the NNG. I wouldn't expect the NNG to standout as a standalone game/puzzle.

[Robin Arnez]

He was also very confused about decide and honestly, rightfully so because the game actually hides what it's actually doing, which is that it applies a "reduction" simp set and then tries the actual decide and doesn't fail if anything fails, so he actually used it once to reduce a + succ b to succ (a + b)...

[Ruben Van de Velde]

I didn't know NNG had decide

[Bhavik Mehta]

I think another relevant point about the lag is that there were 400 people watching the stream, and some of them were trying to play along; at some point the server capacity RAM monitor of the server was above 90% and while I was watching, I didn't see it below 85%

[suhr]

Arthur Paulino said:

I wouldn't expect the NNG to standout as a standalone game/puzzle.

It is an awkward way to use Lean as well. Doing these exercises locally in vs code is nicer and teaches you more.