Port NNG to Lean 4

Stream: lean4

[Huỳnh Trần Khanh]

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

[Kevin Buzzard]

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]

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]

you forgot all semicolons in your message

[Reid Barton]

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

[Sebastian Ullrich]

Kevin Buzzard said:

you forgot all semicolons in your message

I prefer whitespace sensitivity

[Kevin Buzzard]

So we see!

[Matthew Ballard]

(I also use it to tex and lean from my iPad)

[Alexander Bentkamp]

I had worked on the idea of running Lean on a server a while ago, and now I've worked on it a little more. Here is the result so far: https://lean-browser.herokuapp.com/. It may take a while to load because I am not paying for the server. As soon as you see a little "1" in the top left corner, write some Lean code. You can hover over anything that gets underlined. There is no info view yet... And the whole thing seems to collapse after some time of inactivity. But it definitely seems fast enough to work with, at least from Europe where the server is located.

[Alexander Bentkamp]

Oh, and I haven't worked out how to handle multiple users at once. So if you get output that doesn't seem to belong to you, somebody else is playing at the same time :grinning:

[Alexander Bentkamp]

Here is the source code: https://github.com/abentkamp/lean-browser

[Patrick Massot]

Alexander Bentkamp said:

Oh, and I haven't worked out how to handle multiple users at once. So if you get output that doesn't seem to belong to you, somebody else is playing at the same time :grinning:

I'm interested in playing a bit with this idea but I realize I have no idea how stateful web applications work. How can I tell my Apache server that whenever it gets a request on a certain url it should check whether this user already runs Lean and either talk to the corresponding Lean process or start one? Is that something that FastCGI can do? How does something like GitPod handles this? Then how does GitPod or a similar application decides to kill any process? Does it simply wait for a certain time after the last request?

[Alexander Bentkamp]

I've fixed this issue by now. I am using websockets, which is a protocol that can identify different clients much more easily than HTTP. I think Gitpod is using websockets, too. I don't know FastCGI.

[Alexander Bentkamp]

With HTTP, you would need to assign an identifier to each client that the client would include with each request. The identifier should be hard to guess so that you can't steal other people's identity.

[Patrick Massot]

@Alexander Bentkamp Do you have any documentation to recommend about all that?

[Alexander Bentkamp]

It depends on what you would like to use to implement the server. I used NodeJS. Here is a tutorial about that: https://dev.to/codesphere/getting-started-with-web-sockets-in-nodejs-49n0

[Alexander Bentkamp]

Here is documentation about the client side: https://developer.mozilla.org/de/docs/Web/API/WebSocket
And here documentation about the (NodeJS) server side: https://www.npmjs.com/package/ws

[Patrick Massot]

So NodeJS is directly taking connections from the outside world without going through Apache or Nginx or anything like that?

[Patrick Massot]

It's a pity that we can't do that directly in Lean 4 yet. But maybe František Silváši will tell us it actually can.

[Alexander Bentkamp]

You don't need Apache or Nginx. I also used express (https://www.npmjs.com/package/express) in the prototype above, although maybe that wasn't even necessary.

[Alexander Bentkamp]

Implementing the server directly in Lean would be nice :-)

[Siddhartha Gadgil]

I assume that will come when someone writes ffi bindings to something like https://github.com/cesanta/mongoose

[Siddhartha Gadgil]

Or maybe https://www.gnu.org/software/libmicrohttpd/ which seems smaller.

[Alexander Bentkamp]

I think @František Silváši is actually doing it the hard way and implements the protocol from scratch :-).

[Siddhartha Gadgil]

I am familiar with the JVM world so the specific libraries mentioned above are just from naive googleing.

[Alexander Bentkamp]

Anyway, for a usable Lean web interface, it's mostly the client side that needs more love. The server just forwards messages.

[Alexander Bentkamp]

And of course, there is the problem that someone would need to pay for the server.

[Huỳnh Trần Khanh]

This is just a proof of concept, isn't it? Because you didn't do security verification to prevent Lean from damaging the system, right?

[Huỳnh Trần Khanh]

It is possible to write programs in Lean. Programs in Lean can do anything programs in other languages can.

[Alexander Bentkamp]

Hm, yeah, good point. Any ideas how to prevent that?

[Mario Carneiro]

run lean in a container

[Matthew Ballard]

Is that enough?

[Mario Carneiro]

I think that's the standard approach for projects like tio.run and godbolt.org

[Mario Carneiro]

you also need resource limits

[Arthur Paulino]

This question has come up other times and the conclusion is often "run it in a VM/container". I don't have other ideas.

I have memories of someone mentioning that they were trying to build an inoffensive version of Lean 4 without IO

[Mario Carneiro]

yeah I strongly recommend against internal sandboxing here

[Mario Carneiro]

it's way too hard to get right and if you fail your server is hosed

[Matthew Ballard]

If it is not in the browser, then I would just make sure to have a kill switch and nothing of value on the machine.

[Mario Carneiro]

at the very least the machine has credentials to communicate with the website

[Matthew Ballard]

Source code for the playground at go.dev/play. In case anyone wants an example.

[Patrick Massot]

I'm pleased to announce that an early prototype of the first five levels of the natural number game is very temporarily available on http://pat.perso.ens-lyon.org/nng4/. I know that several things are missing (for instance you can easily type unicode characters if you want to right to left rewrite). This was mostly a learning project for me (Lean 4 programming of course but also React that I wanted to learn for future widget writing purposes). It is also a technological demo.

[Patrick Massot]

Note that, when you play the game, Lean runs on my home computer acting as a server. I won't keep this server running forever. So if you read the above message late and can't see anything but a circular loading icon in the middle of a webpage then it means the server is switched off.

EDIT: There is a small issue currently. If you see the circular loading thing forever when the server is meant to be running then you can open about:config in Firefox and toggle network.websocket.allowInsecureFromHTTPS to true.

[Patrick Massot]

Please see https://github.com/PatrickMassot/lean4-game-server, https://github.com/PatrickMassot/NNG4 and https://github.com/PatrickMassot/nng4-interface for a lot more details.

[Johan Commelin]

/me can't see anything but a circular loading icon in the middle of a webpage

[Patrick Massot]

This is extremely weird. Can you try reloading the page?

[Patrick Massot]

It worked yesterday evening with Kevin

[Johan Commelin]

Ctrl-F5 doesn't help

[Riccardo Brasca]

Same here.

[Riccardo Brasca]

Tried with firefox and chrome

[Julian Berman]

Firefox can’t establish a connection to the server at wss://pat.perso.ens-lyon.org:8765/.

[Patrick Massot]

I'll need to fix that but in the mean time you can open about:config in Firefox and toggle network.websocket.allowInsecureFromHTTPS

[Julian Berman]

It still seems to try to upgrade the connection, probably because of HTTPS-only mode... will try from another browser.

[Patrick Massot]

It now works for Johan

[Patrick Massot]

To be clear, what happens is that the website is running over https but it tries to talk to Lean through a non-secure websocket connection. I'll have to understand how to use a secure websocket connection.

[Julian Berman]

It still doesn't work here, (either because I'm on a newer version of FF beta than Johan or because my HTTPS-only mode is on the maximum security which I think isn't the default) but what does work is:

Screen-Shot-2022-10-01-at-10.48.23.png

i.e. just whitelisting your domain to allow non-HTTPS connections. And it's cool!

[Johan Commelin]

I really like the game-play. The way you get hints at a very granular level along the way is super nice!

[Patrick Massot]

That granularity was a very important target. It was one of main pains of the original NNG.

[Patrick Massot]

You can see how tactic-state-triggered messages are registered at https://github.com/PatrickMassot/NNG4/blob/main/NNG/Levels/Level2.lean#L31-L32 for instance.

[Alexander Bentkamp]

Wow, this is beautiful. Great work!

Do you have a way to get a server from your university? I assume I will get access to a university server next week. If you won't get one, I'd go ahead and host it there. It would be a pity to take it down, even if it's just a demo now.

[Patrick Massot]

It would make more sense to get a server from the Hoskinson center (cc @Jeremy Avigad ). But this is a bit premature. We need people to work a bit more on the interface (at least implementing unicode abbreviations and navigating the proof) and more people porting levels. Note that I stopped porting after the first level using induction.

[Patrick Massot]

Then before making wide announcements we would need someone who understand security to have a look at this.

[Alexander Bentkamp]

Ok, right, hosting it at the Hoskinson center would be even better.

It seems that security is not that much of an issue here because the interface to Lean is very restricted. You can just run a handful of tactics, not execute arbitrary Lean code. Anyway, sandboxing the Lean instances might still be a good idea, as Mario proposed above.

[Patrick Massot]

Sure, this is the main reason why I'm not allowing to run any tactic. I also prevents "cheating".

[pcpthm]

I found a way to cheat

rewrite [] <;> sorry

Maybe the server should check the proof for axioms?

[Patrick Massot]

The tactic detection is indeed really basic. This is why I wrote this should be strengthened before advertising it more widely.

[Alexander Bentkamp]

I tried to build nng4-interface locally. I get:

$ npm run build

> nng_interface@0.1.0 build
> react-scripts build

Could not find a required file.
  Name: index.html
  Searched in: /Users/alex/Projects/nng4-interface/public

[Alexander Bentkamp]

Ok, got it to work using this standard React app index.html file: https://github.com/react-cosmos/create-react-app-example/blob/master/public/index.html

[Patrick Massot]

Oops, I forgot the public folder. Indeed I don't think I touched anything in that folder since launching the react app creation script. I just pushed it, sorry about the inconvenience.

[Alexander Bentkamp]

No problem, thanks!

[Patrick Massot]

Could anyone have a look at whether https://pat.perso.ens-lyon.org/nng4ssl/ works without switching off any security thing?

[Adam Topaz]

It seems to work fine for me

[Patrick Massot]

And did you test the previous version?

[Adam Topaz]

No :-/

[Patrick Massot]

Ok, it's still useful information but it would be even better to have someone who had to change something to get the previous version.

[Patrick Massot]

The issue is that it depends on web browser paranoia setting.

[Adam Topaz]

I'll try again with https everywhere turned on

[Patrick Massot]

On Saturday night Kevin had no trouble accessing the non-secure version but on Sunday morning Johan, Julian and Riccardo couldn't.

[Matthew Ballard]

Works for me also (Safari).

[Matthew Ballard]

Also did not test the previous version.

[Adam Topaz]

Adam Topaz said:

I'll try again with https everywhere turned on

https everywhere on and it still works

[Adam Topaz]

So now I have all the default paranoid settings from firefox turned on (https everywhere, full tracker blocking) as well as ublock origin turned on, and things still look good!

[Matthew Ballard]

I tried it on iPadOS Safari and it works there. In my experience, iPadOS has the most stringent security defaults.

[Patrick Massot]

Nice. For people interested in hosting their own game, I pushed a sample https://github.com/PatrickMassot/NNG4/blob/main/gameserver_ssl.py creating a wss server talking to Lean.

[Patrick Massot]

By the way @Frantisek Silvasi the above 50 lines of python are the only non-Lean piece of the Lean 4 NNG prototype. If your planned WebSocket lib in Lean can do that then we could have a 100% Lean setup.

[Patrick Massot]

I would be interested if any real Lean 4 programmer could have a look at what I did at https://github.com/PatrickMassot/lean4-game-server. It was a nice exercise to do this myself (with help of answers to my questions here of course), but now I would be very happy to see the official textbook solution.

[František Silváši 🦉]

The project's being worked on, albeit slowly - I'll be happy to open source this mid-development if someone's interested, although maybe this is a good time to ping @Xubai Wang to see if they're willing to put some license on: https://github.com/xubaiw/BaseN.lean/ :).

Nevertheless, the current state of affairs is such that one can handshake/negotiate a WebSocket connection and I am in the process of finishing/debugging the basic frame structure that this connection requires. I can make few promises wrt. timelines here as this is very much a 'weekend evening' project, but it's not dead.

[Patrick Massot]

It's not really blocking anything, but it would be nice for Leo's talks to be able to say that Lean 4 goes all the way from checking proofs in the game to serving websocket connections.

[Sebastian Ullrich]

We should not abandon the goal of making all this work without a server either though :) . In fact a custom UI like this should make that quite a bit easier since replicating the LSP editor interface always seemed like the biggest hurdle.

[Patrick Massot]

What do you mean by "without a server"? Do you mean running Lean directly in the browser?

[Sebastian Ullrich]

Yes. You're not using the language server, so "export these specific Lean functions to (single-threaded) JS/WASM" is all you need, right?

[Sebastian Ullrich]

Plus "load this restricted set of imports from bundled .olean files". The size of .olean files (Init+Lean) was another in-browser worry, but that shouldn't be an issue for your case I assume.

[Andrés Goens]

Patrick Massot said:

Ok, it's still useful information but it would be even better to have someone who had to change something to get the previous version.

this works for me and the previous version didn't! (and it's really cool)

[Arthur Paulino]

I love the geeky RPG vibes of this version. Well done!

[Patrick Massot]

Sebastian Ullrich said:

Yes. You're not using the language server, so "export these specific Lean functions to (single-threaded) JS/WASM" is all you need, right?

I don't really know. What I I think I need is exactly what is in https://github.com/PatrickMassot/lean4-game-server

[Patrick Massot]

Arthur Paulino said:

I love the geeky RPG vibes of this version. Well done!

Some of it is already in the original NNG, but I wanted to emphasize that Lean 4 meta programming allows to use Lean in a way that doesn't look like Lean, and this is part of it. As explained in https://github.com/PatrickMassot/NNG4#some-game-play-choices, this is completely specific to NNG and not baked in the game server.

[Chris Lovett]

I'm also interested in doing the nng as a lean4 sample that runs in vscode (or in gitpod), see https://github.com/leanprover/lean4-samples/tree/clovett/NaturalNumberGame/NaturalNumberGame.

[Patrick Massot]

What is the motivation for that version?

[Chris Lovett]

mostly trying to decouple from the problem of "web hosting" so we can make progress on the actual content, and providing a place for the code to be checked in so multiple folks can work on it... I saw you posted this link http://pat.perso.ens-lyon.org/nng4/ but the web page you posted didn't respond. Ah, but now I see you have a repo already at https://github.com/PatrickMassot/NNG4 so I'll check that out. Ignore my branch then, unless you want to make this an official lean4-sample. My branch has more of additional world too I think. Should I port that to your repo? are you actively working on this or should I continue with my branch? Your TacticDocs stuff is interesting... I see you are also working on https://github.com/PatrickMassot/lean4-game-server, so I'll check that out also...

[Patrick Massot]

You can try http://pat.perso.ens-lyon.org/nng4ssl/ that has less SSL issues.

[Patrick Massot]

And indeed contributing more levels to https://github.com/PatrickMassot/NNG4 is very welcome. I stopped at the first inductive proof because I was interested in building the framework, not porting levels. I hope Kevin will easily find people interested in porting levels. Also the game server currently does not put levels into worlds. This refinement would be very easy to add, but doing it from the beginning would have been a distraction only.

[Chris Lovett]

ha ha, it works, that's pretty fun, thanks. I found that the rfl after rewrite was unnecessary because rewrite now does a rfl automatically, but your version of the game still acts like the rfl is needed... also the instructions talk about typing "\l" to get a left arrow, but that doesn't work in your Invocation box...

[Mario Carneiro]

removing the rfl after rw is one of the changes that was made in the original NNG to make it more orthogonal for teaching purposes

[Chris Lovett]

and I take it level 5 is not complete yet? It doesn't let me "cast an induction spell"...
image.png

[Patrick Massot]

That's because you didn't read the explanation about how to cast that spell

[Patrick Massot]

The game server is really meant for single line tactics. The new-style induction tactic is completely orthogonal to that, so I wrote a custom induction tactic. And for that game in particular induction won't work anyway because the natural numbers that are used are not an inductive type, see the discussion at https://github.com/PatrickMassot/NNG4#some-game-play-choices

[Mario Carneiro]

The blurb at the end of level 3 mentions rewrite ← h which is problematic both because of the lack of unicode and the missing brackets

[Patrick Massot]

:sad: I tried to find all those missing brackets but obviously they were everywhere since you would never put them for a single rewrite in Lean 3.

[Mario Carneiro]

why not have the NNG version be just rw h with no brackets and no option for multiple rewrite?

[Mario Carneiro]

in level 5 if you write induction_on n with n ih it gives an "unexpected end of input" error

[Chris Lovett]

rw h doesn't work for me in VS Code with latest lean4 ...? It seems I have to write rw [h]

[Mario Carneiro]

that's the lean 3 syntax

[Mario Carneiro]

you were allowed to omit the brackets if there was only one rewrite

[Mario Carneiro]

in lean 4 this was removed

[Chris Lovett]

That seems to go counter to your goal in lean4-game-server of "This discrepancy led to some issues down the road where people got confused by ways tactic have subtly different behaviors in NNG and regular Lean"

[Patrick Massot]

I fixed those issues (sorry for people who were playing, I restarted the server)

[Patrick Massot]

What goes counter to my goal?

[Patrick Massot]

Mario Carneiro said:

why not have the NNG version be just rw h with no brackets and no option for multiple rewrite?

I also considered doing that. But since rewrite already existed it was faster to simply use it. I also wasn't sure how to shadow the existing rw tactic.

[Mario Carneiro]

I assumed that's why you spelled your induction tactic induction_on as well

[Patrick Massot]

Yes

[Mario Carneiro]

I believe (priority := high) on the syntax should suffice

[Chris Lovett]

What goes counter to my goal?

teaching to tactics that you invented just for the game...

[Anatole Dedecker]

Chris Lovett said:

That seems to go counter to your goal in lean4-game-server of "This discrepancy led to some issues down the road where people got confused by ways tactic have subtly different behaviors in NNG and regular Lean"

I think you misunderstood the proposed solution here. Patrick's approach is not to better stick with Lean4, but on the contrary to make a clear distinction between the game and Lean4 so that there is no confusion possible

[Patrick Massot]

Renaming the induction tactic also helps if people want to switch to regular Lean. This way it's clear it's a different tactic.

[Sebastian Ullrich]

It might be easier to use a custom syntax category if you want to deviate from tactic in general

[Chris Lovett]

so do you plan to stick with single line input for the whole game? If so, perhaps my "vs code" version of NNG serves a different goal for folks who want to learn Lean while editing actual lean programs, doing the NNG levels (exercises) as they go with the power of the full lean editor at their finger tips - this is what I personally would prefer but perhaps this then is for a different audience. Question is though would this cause confusion having 2 versions? Should I rename my "lean4-sample" perhaps just call it "NaturalNumbers" or something... since it doesn't really have all the fun "game" elements that the online version has.

[Patrick Massot]

Indeed I think it's better to have a clear distinction between the game and more serious stuff. As I explained in the README, Kevin really wanted this to be a game from the beginning. It became a common first Lean learning step by accident.

[Kevin Buzzard]

Yes we were all surprised about how well it took off.

[Chris Lovett]

Ok, I've renamed the sample to just "Natural Numbers" and prepared it as a leanink style book (removing the game elements). See https://github.com/leanprover/lean4-samples/tree/main/NaturalNumbers. This can be hosted on a simple github pages site like this: https://lovettsoftware.com/NaturalNumbers/index.html

[Chris Lovett]

Now I'm running into an interesting bug in my version and I'm not sure why, I'm finding I need to add this theorem theorem zero_is_0 : MyNat.zero = 0 := by rfl and use it in some places like in Addition Level 4 and I'm not sure why. Is there something missing from MyNat definition that makes it so that I have to do this? I think I implemented OfNat properly because I can do this #eval (zero : MyNat) -- 0, so I'm confused why I need this hack?

[Mario Carneiro]

When you just apply the induction principle for Nat, you end up with the actual constructors of the type, unadorned with any OfNat wrapper. The original NNG had to deal with this as well

[Mario Carneiro]

this is part of why NNG overrides the implementation of induction to handle this

[Mario Carneiro]

the regular induction tactic has the same behavior:

example (x : Nat) : x = x := by
  induction x
-- case zero
-- ⊢ Nat.zero = Nat.zero
-- case succ
-- n✝: ℕ
-- : n✝ = n✝
-- ⊢ Nat.succ n✝ = Nat.succ n✝

[Chris Lovett]

Ok, so it sounds like my having to add rw [zero_is_0] is not a bug, but things are working normally then. If so, I will try and add some explanation for this. I also found that the simp example didn't work in Lean 4 with the Level 6 example of (((a+b)+c)+d)+e=(c+((b+e)+a))+d, is this because I have not completed the AddMonoid instances and does that somehow extend the power of simp?

[Mario Carneiro]

you need to simp with add_assoc, add_comm, add_left_comm either by passing them to the simp call or marking the lemmas as @[simp]

[Chris Lovett]

I already have this: attribute [simp] zero_add add_assoc add_comm succ_add add_succ succ_eq_add_one one_eq_succ_zero add_right_comm but there is no add_left_com in the original NNG?

[Chris Lovett]

But interestingly, when I got to multiplication level 9 that example worked:

example (a b c d e : MyNat) :
  (((a*b)*c)*d)*e=(c*((b*e)*a))*d := by
  simp

[Chris Lovett]

and this has a left_comm attribute [simp] mul_assoc mul_comm mul_left_comm so I went back to level6 and changed it to this, and now it works too :-)

attribute [simp] add_assoc add_comm add_left_comm

example (a b c d e : MyNat) :
  (((a+b)+c)+d)+e=(c+((b+e)+a))+d := by
  simp

[Kevin Buzzard]

Yeah, this was a problem in Lean 3 NNG; 0 is has_zero.zero whereas induction would spit out nat.zero which printed differently and confused users. here is where I change induction so that it does usual induction and then runs dsimp with a simp set including this which means that users don't ever see the problem.

[Alexander Bentkamp]

Sebastian Ullrich said:

Yes. You're not using the language server, so "export these specific Lean functions to (single-threaded) JS/WASM" is all you need, right?

Do you have some hints on how to do this?

[Sebastian Ullrich]

I think the most promising way to an official Emscripten build of Lean was last discussed in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/wasm.20nix.20emscripten.20build/near/271113368. Though if someone is seriously considering completing that work, we should first chat with @Leonardo de Moura about .olean platform portability expectations.

[Chris Lovett]

I found this Lean 4 solution to Power World Level 8, not using "Ring", but is there a simpler one?

lemma add_squared (a b : MyNat) :
  (a + b) ^ two = a ^ two + b ^ two + 2 * a * b := by
  rw [two_eq_succ_one]
  rw [one_eq_succ_zero]
  repeat rw [pow_succ]
  repeat rw [pow_zero]
  repeat rw [one_mul]
  rw [mul_add]
  repeat rw [add_mul]
  rw [←one_plus_one]
  repeat rw [add_mul]
  repeat rw [one_mul]
  simp

See lean ink version

I couldn't get Mathlib.Tactic.Ring to work here as shown in Lean 3 NNG.

[Chris Lovett]

I'm happy to report the entire NNG is now ported to lean4, here's the raw source code :

• https://github.com/leanprover/lean4-samples
  which is published in a non-interactive-game format as a tutorial here:

• https://lovettsoftware.com/NaturalNumbers/TutorialWorld.lean.html

The effort was a great learning experience and I have to thank Mario Carneiro, Heather Macbeth for much help and guidance along the way.

Note that this is not a 1:1 port as some tactics are missing still, like cc so the port includes rewriting proofs so they do not depend on these missing tactics. I think cc was the only real big missing piece I ran into. I also did not use ring since it was more work to setup. But if someone wants to go back and put ring back in PR's are welcome.

TBD: the stuff about collectable "instances" of things that use your proofs is not implemented because some of that stuff is still missing from mathlib4. If you search the web page for BUGBUG you will see where those TBD work items exist.

[Chris Lovett]

Oh, and having gone through the whole thing with a fine tooth comb, I have to say huge thanks to Kevin Buzzard for the original content - it is definitely well thought out and presents things in a really clear and enjoyable way. I only found 1 typo: your your goal

[Chris Lovett]

This is a map of the tactics covered and where they are first introduced:

image.png

[Kevin Buzzard]

The reason I push for "naturals are a semiring" before starting on order theory is that to prove naturals are a semiring you only need to know three tactics! I found this extraordinary. I remember telling @Jeremy Avigad at the time and him replying "sure, it's just equational reasoning" and me not having a clue what that even meant.

[Kevin Buzzard]

It was conversations like this which made me realise that 25 years of being a professional number theorist doesn't teach you anything about how mathematics actually works

[David Michael Roberts]

In classic category theorist fashion, I guess I get to say "number theory is really just the study of the free semiring on one generator"...

More seriously, there is such impressive richness in our playground, even from humble origins.

[Jeremy Avigad]

What I had in mind was Birkhoff's theorem:
https://en.wikipedia.org/wiki/Variety_(universal_algebra)
It tells us that lots of interesting structures can be axiomatized by equations, and that consequences of those equations can be proved with just rw.
https://en.wikipedia.org/wiki/Birkhoff%27s_theorem_(equational_logic)

[joaogui1 (he/him)]

@Patrick Massot given that Chris Lovett ported the content to Lean4 are you just going to use his port for the content and keep working on the interface? What's your plan?

[Patrick Massot]

Chris's effort is completely orthogonal to what is needed for the game. He wanted a set of Lean files to edit normally in VSCode, using an inductive type for natural numbers and Lean regular tactics. Also, in the game version, a lot of the work is to update the explanations from the Lean 3 game to remove unneeded parts and, much more importantly, to give explanations in response to tactic states.

[joaogui1 (he/him)]

Got it!