building your own Lean game

Stream: Lean for teaching

[Emily Riehl]

@Alexander Bentkamp suggested I use this channel for some questions related to building my own Lean game.

[Emily Riehl]

Firstly, has anyone devised a method for building a level that allows students to attempt to prove a statement that can't be proven? I think this might be helpful at various stages to make various pedagogical points.

For example, I've just written a level that attempts to explain the default interpretation of P -> Q -> R as well as the inequivalence between (P -> Q) -> R and P -> (Q -> R). It occurred to me that one way to drive this home would be to ask them to prove P -> Q -> P and/or P -> Q -> Q and then give them a chance to try (and fail) to prove (P -> Q) -> P and/or (P -> Q) -> Q.

[Alexander Bentkamp]

The natural number game contains a level that asks you to prove Fermats last theorem: https://github.com/leanprover-community/NNG4/blob/main/Game/Levels/Power/L10FLT.lean

[Jon Eugster]

and if you need a way to successfully solve unsolvable levels, you can also take inspiration from the NNG.

[Emily Riehl]

This is definitely inspiring, but I don't quite understand it. Did the NNG implement a new tactic "xyzzy" or just make up a name for an existing tactic? Either way, how would I set this up myself in my game?

[Kenny Lau]

https://github.com/leanprover-community/NNG4/blob/4e8b2e1c15c7882a277c651a6f54db4ee858d50d/Game/Tactic/Xyzzy.lean#L9

[Emily Riehl]

I'm trying to write a comment to explain how to type ⟨. I've written

Conclusion "Alternatively, you can type `exact ⟨p,q⟩' using '\\<' and '\\>' to type the angle braces."

but it renders as < rather than \< (with the backslash missing). How do I fix this?

[Alexander Bentkamp]

Just a guess: maybe 4 backslashes do the trick?

[Emily Riehl]

Thanks, yes!

[Aaron Liu]

You need to escape the escape

[François G. Dorais]

Also: raw strings https://lean-lang.org/doc/reference/latest//Basic-Types/Strings/#raw-string-literals

[Jon Eugster]

François G. Dorais said:

Also: raw strings https://lean-lang.org/doc/reference/latest//Basic-Types/Strings/#raw-string-literals

saved a memo for this: lean4game#351

[Alex Kontorovich]

Quick question: Is it possible to include images in the text of a game? I see in the docs support for CoverImage "images/cover.png", but is it possible to put images elsewhere? Thanks!

[Alex Kontorovich]

Another question: In the Natural Number Game, rw [h] is somehow weakened compared to the rw of Mathlib (in particular, it needs an extra rfl at the end, whereas Mathlib's rw tries to run that automatically). I need Mathlib's Real Numbers, but would like to have NNG's rw... I don't suppose that's possible?

[Kevin Buzzard]

Sure it's possible, just copy NNGs rw tactic into your project. It's probably called something like NNG/Tactic/Rw.lean and if you import that file then hopefully you'll have exactly what you want

[Alexander Bentkamp]

Re: images
https://github.com/leanprover-community/lean4game/blob/main/doc/hints.md#images
I didnt know this was already implemented until just now!

[Alex Kontorovich]

Kevin Buzzard said:

Sure it's possible, just copy NNGs rw tactic into your project. It's probably called something like NNG/Tactic/Rw.lean and if you import that file then hopefully you'll have exactly what you want

I guess I also want to have access to the rest of Mathlib, and I can't have two things called rw. Oh well, I'll use Mathlib's version. Thanks!

[Alexander Bentkamp]

Hm, are you sure you cant have two rw tactics? Maybe setting a higher priority for the new rw tactic could work?

[Alex Kontorovich]

I guess I wouldn't want to confuse students with two different behaviors? Let it be the stronger one, if that's what Mathlib does...

[Alex Kontorovich]

It looks like the image Markdown solution doesn't work? I added <img src=\"https://url.com/to/image\"/> to my file, and I just see the text...?

[Alex Kontorovich]

(of course with a link to an actual image)

[François G. Dorais]

IIRC rewrite instead of rw does what the NNG rw does.

[Alexander Bentkamp]

Maybe @Jon Eugster knows more about the state of including images?

[Jon Eugster]

Alex Kontorovich said:

Kevin Buzzard said:

Sure it's possible, just copy NNGs rw tactic into your project. It's probably called something like NNG/Tactic/Rw.lean and if you import that file then hopefully you'll have exactly what you want

I guess I also want to have access to the rest of Mathlib, and I can't have two things called rw. Oh well, I'll use Mathlib's version. Thanks!

You should be able to! NNG and Robo both do that a lot. Make sure your custom rw tactic has a custom different internal name in Lean. You can take the NNG's rw (which does not use rfl) as an example.

[Jon Eugster]

Alex Kontorovich said:

It looks like the image Markdown solution doesn't work? I added <img src=\"https://url.com/to/image\"/> to my file, and I just see the text...?

If I remember correctly, not all texts e verywhere might be markdown (wich is a bug) and this was called a hack because the URL might be different depending on how you access the game (local/production) and thus they don't fully work. I don't think I've ever implemented full images support

[Alex Kontorovich]

Thanks! How hard do you think it would be to implement image support (at a basic level, just in the "intro"s to Levels)?

[Emily Riehl]

There's a TheoremTab that allows me to define symm under both And and Or, for instance. Is there a similar DefinitionTab to split definitions into tabbed lists?

[Chris Henson]

Emily Riehl said:

There's a TheoremTab that allows me to define symm under both And and Or, for instance. Is there a similar DefinitionTab to split definitions into tabbed lists?

I was working on a Lean game recently (for a lambda calculus) and had a similar question. Are there any utilities for displaying available definitions to the user? It would be nice for to have something both tied to the code and available for later recall.

[Emily Riehl]

I'm having some difficulty also using NewTheorem. I have something like

/--
For propositions `P`, `Q`, and `R`, `And.curry` is a proof that `P ∧ Q → R` implies `P → Q → R`.
-/
TheoremDoc And.curry as "curry" in "And"

Statement And.curry {P Q R : Prop} (h : P ∧ Q → R) : P → Q → R := by
  intro p
  intro q
  apply h
  exact ⟨p, q⟩

NewTheorem And.curry

The hope is that they could use this in proving later that this implication is an if and only if. But because And.curry isn't a mathlib name (I have no idea whether this theorem is in mathlib) when I try to use this a few levels later, Lean doesn't seem to recognize the definition. Or is the issue that I need to build something?

[Dan Velleman]

Is this inside a namespace? If so, then I think you need to use the full name of the theorem in TheoremDoc, including the namespace. Also, I don't think you need to use NewTheorem in this situation.

[Alexander Bentkamp]

Do you import this level from the later levels?

[Emily Riehl]

Alexander Bentkamp said:

Do you import this level from the later levels?

No, each file just imports Game.Metadata. Is there a way for user generated names to automatically get added there?

[Emily Riehl]

Or maybe I should just avoid user generated theorem names?

[Alexander Bentkamp]

Just import the level file in the later level files, where you need the theorem.

[Emily Riehl]

This is a pretty large game with partial rather than linear dependencies. I either want a more automated solution or I'll do without. I'd rather have all the definitions in the library be actual terms that can be used in any subsequent level or not have them there.

[Emily Riehl]

Dan Velleman said:

Is this inside a namespace? If so, then I think you need to use the full name of the theorem in TheoremDoc, including the namespace. Also, I don't think you need to use NewTheorem in this situation.

Can you tell me why NewTheorem isn't needed? Clearly I don't really understand its functionality...

[Dan Velleman]

I'm going by the instructions here: https://github.com/leanprover-community/lean4game/blob/main/doc/create_game.md.

Those instructions say: "You can give your exercise a name: Statement my_first_exercise (n : Nat) …. If you do so, it will be added to the inventory and be available in future levels."

When I wrote the Set Theory Game, I didn't need to use NewTheorem when I had a Statement with a name. Also, I had each level import the previous level, and the first level of each world imported the previous world. But the display of the worlds when you play the game doesn't show a linear order--the dependencies displayed are computed based on which tactics and theorems are used.

[Emily Riehl]

Do you have any idea whether this works for definitions in addition to theorems? I'm trying

/--
The `swap` function exchanges the inputs of a function of two variables. For a function with two variables `f : A → B → C`, `Function.swap f : B → A → C` is the function that sends `b : B` and `a : A` to `f a b : C`.
-/
DefinitionDoc Function.swap as "Function.swap"

Introduction "An element of type `A → B → C` can be thought of as a function of two variables. Given `f : A → B → C`, `a : A`, and `b : B`, `f a b : C` denotes `f` applied first to `a` and then to `b`. From a function of type `A → B → C`, we can define a function of type `B → A → C` by swapping the order of the input variables.
"

Statement Function.swap {A B C : Type} : (A → B → C) → (B → A → C) := by
  Hint (hidden := true) "When in doubt, start defining a function by using the tactic `intro` followed by your preferred variable name."
  intro f
  Hint (hidden := true) "When in doubt, start defining a function by using the tactic `intro` followed by your preferred variable name."
  intro b
  Hint (hidden := true) "When in doubt, start defining a function by using the tactic `intro` followed by your preferred variable name."
  intro a
  Hint (hidden := true) "Look carefully at the order of the arguments of `{f}`."
  exact f a b

But I'm getting an error Missing Lemma Documentation: Function.swap Add LemmaDoc Function.swap somewhere above this statement

Indeed, because I've labeled something defined by Statement, the game seems to think this is a theorem, and it appears on my list of theorems (with a missing doc) rather than on the list of definitions. But when I import this file into later files I am able to use the definition (unfolding it, etc).

[Jon Eugster]

so as Dan correctly mentioned, every named Statement will be added automatically as a theorem. NewTheorem is used for adding external theorems to the game, e.g. Mathlib statements you want to use in the level where you write NewTheorem.

There isn't a direct, automated way to add your Statement as a definition. For one because we only featured tactic-proofs and constructing definitions in tactic mode has always been considered bad as far as I know.

However, you could do the following:

• do not name the Statement where you "proof" (construct) your Function.swap
• In the next level, make sure you have imported Function.swap from somewhere (Mathlib, or just write it into that file as def Function.swap; and add NewDefinition Function.swap in this next level

(PS: if you name your Statement and give it a _docstring_, it should automatically take that as the doc)

[Jon Eugster]

Emily Riehl said:

Alexander Bentkamp said:

Do you import this level from the later levels?

No, each file just imports Game.Metadata. Is there a way for user generated names to automatically get added there?

And yes, since a game is a normal Lean project, you do need to import the file which defines something in the file where you want to use something. There's no (resonable?) way around that

(What we can and will fix soon, is that the player should have everything accessible regardless of imports. e.g. the player should be able to use an unlocked theorem everywhere later, even in earlier levels which they re-attempt later. That will affect the player experience, but will not change anything when you open the game as Lean project to work on it.)

[Jon Eugster]

Emily Riehl said:

There's a TheoremTab that allows me to define symm under both And and Or, for instance. Is there a similar DefinitionTab to split definitions into tabbed lists?

So far not because we never had enough definitions, but could be implemented fairly easily, if needed

[Jon Eugster]

Chris Henson said:

I was working on a Lean game recently (for a lambda calculus) and had a similar question. Are there any utilities for displaying available definitions to the user? It would be nice for to have something both tied to the code and available for later recall.

Im afraid, currently not, but that's a good idea

[Jon Eugster]

@Emily Riehl something I think we could add with basically no effort would be an optional argument Statement (asDef := true) Function.curry : .... := by which would add the statement automatically as a definition (instead of theorem) for later levels. Would that be useful?

[Emily Riehl]

Jon Eugster said:

Emily Riehl something I think we could add with basically no effort would be an optional argument Statement (asDef := true) Function.curry : .... := by which would add the statement automatically as a definition (instead of theorem) for later levels. Would that be useful?

Yes, thanks Jon Eugster. This would be great.

[Alex Kontorovich]

Two quick questions:

• I can't seem to add the have tactic in usual incremental way, TacticDoc have and NewTactic have give the error: "unexpected token 'have'; expected command". So how do I show the syntax for have in the list of "reminders" next to the other tactics? And
• Is it possible to erase one's work on one level (and presumably everything after it), but not everything before it? Say I want to see how level 10 works, but don’t want to replay 1-9, and don’t want to relax the rules (that is, I don't want to "cheat" when I play level 10) -- is there a way to do that?
  Thank you!

[Aaron Liu]

Alex Kontorovich said:

• I can't seem to add the have tactic in usual incremental way, TacticDoc have and NewTactic have give the error: "unexpected token 'have'; expected command". So how do I show the syntax for have in the list of "reminders" next to the other tactics?

Have you tried the french quotes?

[Aaron Liu]

That means, instead of writing TacticDoc have, write TacticDoc «have»

[Alex Kontorovich]

Ah, the old French quotes trick! I should've guessed... :) Works like a charm, thanks!

[Emily Riehl]

Now that I've hidden a few worlds, I only have one theorem tab, which is supposed to be "And". But it's invisible from the current web version of the game:

https://adam.math.hhu.de/#/g/emilyriehl/ReintroductionToProofs

Is this the expected behavior, or am I using it wrong?

[Jon Eugster]

That is indeed expected behaviour if there is only a single tab. The thought was that it might be desired to design a game where you don't need tabs at all

However I'm not opposed to changong that behaviour if desired...

[Emily Riehl]

Jon Eugster said:

so as Dan correctly mentioned, every named Statement will be added automatically as a theorem. NewTheorem is used for adding external theorems to the game, e.g. Mathlib statements you want to use in the level where you write NewTheorem.

There isn't a direct, automated way to add your Statement as a definition. For one because we only featured tactic-proofs and constructing definitions in tactic mode has always been considered bad as far as I know.

However, you could do the following:

• do not name the Statement where you "proof" (construct) your Function.swap
• In the next level, make sure you have imported Function.swap from somewhere (Mathlib, or just write it into that file as def Function.swap; and add NewDefinition Function.swap in this next level

(PS: if you name your Statement and give it a _docstring_, it should automatically take that as the doc)

Following @Alexander Bentkamp's suggestion I'm now working on my later levels in a development branch, starting with function world. These files used to compile fine (at least when I was playing the game locally) but now I'm getting an error message that didn't appear before:

For

Statement {A : Type} : A → A := by

I get the error type of theorem is not a proposition which I certainly agree with. Should I be using something other than Statement here?

[Kevin Buzzard]

Oh wow! I had levels of this form in the Lean 3 version of NNG ("function world" or something), I had an entire world of constructing functions with intro and apply in preparation for using the same tactics to prove theorems about Props. But I decided to ditch them in Lean 4 NNG and just use concrete props, so never tried something like this.

[Emily Riehl]

Yeah my idea is to try teach informal dependent type theory in a lightweight way so as not to (overly) corrupt the youth. So definitely the Curry Howard correspondence. Maybe inductive types (depending on how strong the students are, which I'll start to find out tomorrow).

[Jon Eugster]

Let me look at that today. I think that might be because recent Lean+mathlib have more and more Linters activated by default, and they might not be disabled in your game. That's certainly not ideal.
You'll get a proper way to write non-Prop levels within in the next days!

[Emily Riehl]

Jon Eugster said:

Let me look at that today. I think that might be because recent Lean+mathlib have more and more Linters activated by default, and they might not be disabled in your game. That's certainly not ideal.
You'll get a proper way to write non-Prop levels within in the next days!

Thanks. Really appreciated. This is kind of crucial for my course plan... :)

[Emily Riehl]

@Jon Eugster is there someone else I should loop into the conversation about this? If it doesn't look like I'll be able to get my type-theory based levels restored in the next week, I need to start making a new plan for my second class meeting.

[Jon Eugster]

Sorry I didn't realise you literally already started your course and are running on less than a week prep. I'll PR the fixes to your repo tomorrow during the day. When's your next class?

[Jon Eugster]

The fix is building now and should be online in about an hour.

@Emily Riehl in about an hour, you should be able to just call lake update in your game repo and it should work (that should only change the commit SHA of GameServer in your lake-manifest.json). Ofc, you should also pull the newest version of lean4game if you run the server locally. If you do have further problems, it might be an idea to give me access to your private repo, the levels which are in the public repo aren'r really affected.

[Jon Eugster]

I'm sorry you have to be one of the guinea pigs which try out the updated v4.22.0 version of the game server. there have been significant changes to finally get past v4.7.0 and I'm working full-time nowadays.

[Emily Riehl]

Thanks @Jon Eugster really appreciated. I'm not sure I managed to correctly follow the instructions though.

I added the GameSkeleton repo as upstream and force merged that into my clone. This did end up changing the lake-manifest.json. But I don't think this is what you meant by "pull the newest version of lean4game". Could you clarify how I should do this?

Btw the broken dev branch is now publicly visible and its version of the lake-manifest.json file is here

[Jon Eugster]

I've DMed the PR with the changes. It is lake update -R, I forgot lake still had this option -R which has the (arguably) wrong default when update is called.

[Emily Riehl]

Should I copy across this version of the lake-manifest file to the main branch? At some point I'll start merging version of the levels currently in the dev branch into the main branch.

[Emily Riehl]

Actually this still seems to be broken. The dev branch of the repository compiles just fine now but when I play the game locally I'm unable to solve any of the levels (even using the same code from the source files).

[Emily Riehl]

For example here's the first constructive level

import Game.Metadata

World "FunctionWorld"
Level 1

Title "Identity Function"

/--
For a type `A`, `id : A → A` is the function defined by sending `a : A` to `a : A`.
-/
DefinitionDoc id as "id"

Introduction "The simplest example of a function is the identity function, which may be defined for any type `A`. The identity function
`id : A → A` is defined to carry any element `a : A` to itself.

To define a function `f : A → B` one must define a rule that converts an arbitrary element `x : A` to some element of type `B`. Start by typing `intro x` to add an arbitrary element `x : A` to the context and update the goal to a term of type `B`."

Statement {A : Type} : A → A := by
  Hint "To define a function, in this case a term of type `{A} → {A}`, one must define a rule to convert an arbitrary element `x : {A}` to some element of type `{A}`. Start by typing `intro x` to add an arbitrary element of type `{A}` to the context."
  intro x
  Hint "Now the goal is an element of type `{A}`, which should be thought of as result of applying the function to the element `{x} : {A}`. In the case of the identity function, we want to return `{x} : {A}` again which is done by typing `exact {x}`."
  exact x

Conclusion "You can solve this level in one level by just giving the entire formula for the function as
`exact fun x ↦ x`, using `\\mapsto` to type `↦`. This tells Lean that the answer is the function defined on an input element `x` to have an output value `x`."

NewDefinition id

[Emily Riehl]

When I demo the game by typing intro x it seems to crash typewriter mode. When I switch to editor mode I can type the full two line proof intro x; exact x and at the end it tells me no goals. But there's a red squiggly line under the intro x with the message

type of theorem 'the_theorem._@.Game.Metadata._hyg.2' is not a proposition
  {A : Type} → A → A

Also, despite the no goals, the game does not seem to think the level is complete and in particular won't let me advance to the next one.

[Jon Eugster]

https://github.com/emilyriehl/ReintroductionToProofs/pull/2

Emily Riehl said:

Should I copy across this version of the lake-manifest file to the main branch?

Yes, your main branch should have the same manifest as the dev branch, i.e. the manifest from the PR above

[Emily Riehl]

Thank you @Jon Eugster. This is REALLY REALLY appreciated.

[Alex Kontorovich]

The first lecture is up! https://alexkontorovich.github.io/2025F311H Any comments/suggestions are very welcome (by DM, if you prefer, or better yet, by PR)!

[Alex Kontorovich]

And thanks again to everyone for helping make it possible!

[Derek Rhodes]

@Alex Kontorovich, thank you for posting your real analysis lecture videos. I'm having a lot of fun working through the course and am enjoying the historical interludes.

[Jon Eugster]

Emily Riehl said:

There's a TheoremTab that allows me to define symm under both And and Or, for instance. Is there a similar DefinitionTab to split definitions into tabbed lists?

Btw, this is now in the v4.23.0 version: You can sort Definitions and Tactics into tabs, too, if you'd like. Same syntax as for theorems:

/-- defined as `Injective f ∧ Surjective` -/
DefinitionDoc Function.Bijective as "Bijective" in "Fun"

[Emily Riehl]

Awesome. But either I'm using it wrong

DefinitionTab "Empty"

/--
For any type `A`, there is a function `Empty.elim : Empty → A` expressing the elimination rule of the empty type.
-/
DefinitionDoc Empty.elim as "elim" in "Empty"

NewDefinition Empty.elim

or I don't know how to update to the v4.23.0 version (or figure out what version I'm on). I ran git pull upstream main which did something then lake update which did not appear to do anything.

[Jon Eugster]

The chosen workflow for updating (which I promote in the Lean projects I'm working on) is:

1. manually change the version in lean-toolchain to leanprover/lean4:v4.23.0
2. run lake update -R
3. done.

Looking at your repo's dev branch, you need to do (1.)

(note: this only works in projects which have there lakefile.lean configured correctly. Your game is configured that way which you could see by the usage of def leanVersion : String := s!"v{Lean.versionString}" in the lakefile)

[Jon Eugster]

(I'm not sure you should run git pull upstream main unless you know what you're doing. It depends on how your git project is set up, i.e. whether a remote named upstream is defined. For your mathlib fork, you probably have set this up correctly with the main branch pointing at an upstream/main branch. I wouldn't be sure what your setup is in your game's local clone. You can check with info-prints like git remote and git branch -vv)

[Jon Eugster]

(btw -R might be superfluous, but in my head it stands for "[R]eally do it!". There are some situations where lake update without the -R doesn't actually do the update.)

[Emily Riehl]

Jon Eugster said:

The chosen workflow for updating (which I promote in the Lean projects I'm working on) is:

1. manually change the version in lean-toolchain to leanprover/lean4:v4.23.0
2. run lake update -R
3. done.

Looking at your repo's dev branch, you need to do (1.)

(note: this only works in projects which have there lakefile.lean configured correctly. Your game is configured that way which you could see by the usage of def leanVersion : String := s!"v{Lean.versionString}" in the lakefile)

I don't know if my lakefile is configured incorrectly but this broke something in my vscode installation. I'm getting an error:

Error while checking Lean version: Lean version 'leanprover/lean4:v4.23.0' of Lean project '/home/node/game' is not installed. Reason: Installation failed. Error: error: Permission denied (os error 13)

[Emily Riehl]

I can't find the refresh lean server in the command pallette (where it usually is).

[Emily Riehl]

I can find something called setup update release channel lean version but when I try to do this it tells me the permission is denied

[Emily Riehl]

I'm teaching tomorrow so it's a bad time for Lean to be broken... :cold_sweat:

[Dan Velleman]

@Emily Riehl , are you using a container to test your game locally? I have sometimes experienced the "permission denied (os error 13)" error when I was doing that. Have you tried deleting the container and rebuilding it?

[Dan Velleman]

@Jon Eugster , could this be related to this issue: https://github.com/leanprover-community/lean4game/issues/296
There is a proposed fix there, but I don't think it has been implemented, has it?

[Emily Riehl]

I am, so that might be the problem. Let me see if I can figure out how to delete the container.

Update: Thanks @Dan Velleman . I think that was the issue.

[Dan Velleman]

Glad to hear it worked.

[Emily Riehl]

Back with another issue. The theorems part of the library of my game broke sometime in the last few days. The tactics and definitions part of the library are fine.

(I haven't yet implemented the new definition tabs mentioned by @Jon Eugster because I still can't figure out how to get it to work.)

Has this happened to anyone else? I'm not sure what I'm doing wrong.

[Emily Riehl]

For example this is the source code for level 1 of Classical World

TheoremTab "Classical"

/--
For any proposition `P`, `Classical.byContradiction : ¬ ¬ P → P` proves that if `P` is not false, then `P` is true.
-/
TheoremDoc Classical.byContradiction as "byContradiction" in "Classical"

NewTheorem Classical.byContradiction

and this is from level 2:

/--
For any proposition `P`, `Classical.em P : P ∨ ¬ P ` proves that `P` or `¬ P` is true.
-/
TheoremDoc Classical.em as "em" in "Classical"

NewTheorem Classical.em

[Dan Velleman]

@Emily Riehl , what you're doing looks right to me. I never had that problem.

Perhaps you've already thought of this, but since you say it used to work, I'd be inclined to remove some worlds from the game (easy to do by commenting out some lines in your Game.lean file) and see if the theorem library starts working again. If so, add worlds back in to see which world broke it.

[Jon Eugster]

That might be a backwards compatibility issue from my side, I'll check. Is it broken only on the live server or locally alike?

[Jon Eugster]

Emily Riehl said:

Back with another issue. The theorems part of the library of my game broke sometime in the last few days.

Fixed :) sorry for the inconvenience

[Jon Eugster]

Emily Riehl said:

(I haven't yet implemented the new definition tabs mentioned by Jon Eugster because I still can't figure out how to get it to work.)

https://github.com/emilyriehl/ReintroductionToProofs/pull/4

[Emily Riehl]

Thanks @Jon Eugster. Can you explain what you've done? I ask because I want to merge this into the main branch, not the dev branch (which in fact, after this coming Monday's class, I'm just going to get rid of).

[Jon Eugster]

For moving the definitions into tabs? You just add in "Tabname" at the end of the DefinitonDoc command. You should also get this info if you look at the (hover) docstring of DefinitionDoc.

(As for the broken theorems bug, that was purely an error on our side and I fixed it by updating the version of lean4game which runs at adam.math.hhu.de)

[Emily Riehl]

I'm back with something weird I'd like to do with a Lean game. Is it possible to have levels involving structures?

E.g., I'd love to build a level with this goal:

Statement {A B : Type} : (A × B) ≃ (B × A) := by sorry

but I'm getting some sort of error (a red underline of the equivalence symbol). Typing Equiv (A × B) (B × A) instead gives a more comprehensible error message

Unknown identifier `Equiv`
Error code: lean.unknownIdentifier

[Kevin Buzzard]

Are you just missing an import or is the problem worse than that?

[Kevin Buzzard]

(looks like it's Mathlib.Logic.Equiv.Defs)

[Kevin Buzzard]

(or probably Mathlib.Logic.Equiv.Basic if you want a nonzero amount of API)

[Emily Riehl]

When I try to import a mathlib file I get an error

unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:

[Emily Riehl]

I made a working level like this but I feel like it's going to be hard to guide the students to the proof in the Lean game interface

import Game.Metadata

World "EquivalenceWorld"
Level 1

Title "Testing"

Introduction "This is probably a bad idea
"

/-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
structure Equiv (α β : Type) where
  toFun : α → β
  invFun : β → α
  left_inv : invFun ∘ toFun = id
  right_inv : toFun ∘ invFun = id

@[inherit_doc]
infixl:25 " ≃ " => Equiv

Statement {A B : Type} : (A × B) ≃ (B × A) := by
  refine ⟨fun p ↦ ⟨p.2, p.1⟩, fun p ↦ ⟨p.2, p.1⟩, ?_, ?_⟩
  rfl
  rfl

Conclusion "This is probably a bad idea"

[Emily Riehl]

The problem is I don't know the best way to access the fields of the structure. I tried constructor but it gives them to me in a bad order (with the coherences first). After filling in the definitions of toFun and invFun in the 3rd and 4th goals they don't seem to compute in the 1st and 2nd goals (i.e., rfl fails).

[Emily Riehl]

So maybe this whole thing is a bad idea?

[Kevin Buzzard]

Hmm, I am definitely doing import Mathlib.Stuff in NNG4 (see e.g. this file but pretty much everything other than the "write the levels and the text descriptions" in that repo was done by other people. NNG4 has a lakefile.lean which I find totally intimidating but one of the lines in it is require "leanprover-community" / mathlib @ git leanVersion which presumably is what's getting import Mathlib.stuff working.

Certainly though it's not impossible to just copy chunks out of mathlib in your own game.

Maybe constructor is a good tactic to start off "proving" that Statement? Then hopefully you'll just get 4 goals. The problem will be that students will be then defining data in tactic mode and this can go wrong, e.g. making fun p ↦ ⟨p.2, p.1⟩ in tactic mode might involve a student going intro p and then cases p and there might either be an incomprehensible error at that point or you'll end up with a function you can't prove anything about. Maybe your refine approach is best?

[Emily Riehl]

I like the idea of starting with constructor but it gives me the goals in the wrong order. Is there a way to force the goals to come out with the first goal of defining the functions?

[Jon Eugster]

It definitely should be possible to talk about structures in the games. We did this in Robo and had some thoughts about how to work with them in the game framework.

(I need to look up the details later, I think one thing was to use fconstructor which does not reorder elements, but there might be a few more workarounds we did)

As for mathlib, you should require it in the lakefile as Kevin said, if you haven't done that already.

[Emily Riehl]

The lakefile suggestion works but fconstructor is giving me an unknown tactic error. Any suggestions would be welcome!

[Kevin Buzzard]

import Mathlib.Tactic.Constructor? I jumped to definition on an fconstructor in mathlib and this is where it took me, at any rate...

[Jon Eugster]

We have the following Lean file somewhere in Robo where it is imported by Game/Metadata.lean. (import fconstructor from mathlib and overwrite constructor to use fconstructor instead)

modifided constructor from Robo

import Mathlib.Tactic.ExtendDoc
import Mathlib.Tactic.Constructor

open Lean Meta Elab Tactic

namespace Game

@[inherit_doc Lean.Parser.Tactic.constructor]
macro (name := constructor) "constructor" : tactic =>
  `(tactic| fconstructor)

extend_docs Game.constructor after "The variant used in the Robo game is called
`fconstructor` in Mathlib. The only difference is the real `constructor` sorts
the goals in a way not ideal for the game."

[Jon Eugster]

And here is a bit a more elaborate level example: We want to show that something is a Submodule. This involves predefining some data, otherwise the exercise would simply be "construct any Submodule you can think of"

Screenshot 2025-09-29 at 20.04.40.png

Code snippet

Statement FirstColumnSumZero
    (preamble := refine' {carrier := M, ..} <;> try dsimp only)
    {n : ℕ} [NeZero n] :
    let M := {A : Mat[n,n][ℝ] | ∑ i, A i 0 = 0}
    Submodule ℝ Mat[n,n][ℝ] := by
 -- proof: 3 different goals, one for each property to prove

• There is the (preamble := ...) argument where you can define arbitrary tactic-code which is executed before the student can start the level.
• using let M := ... inside the statement results in M being displayed under "Objects" (ignore the bug, that you don't see the definition of M up there, that should be fixed...)
• The student starts in a state with three open goals which are the three remaining fields of the structure.

However, I agree this is certainly more about how far you can push the choices made at lean4game about single-line tactic proofs and there are fair limitations to that approach...

[Jon Eugster]

Screenshot 2025-09-29 at 20.12.25.png

It should display the let values like this

[Jon Eugster]

(oh and ignore the Mat[n,n][ℝ] syntax, that's just a custom abbreviation to get "normal" matrices)

[Emily Riehl]

Thanks. I'll see if I can figure out how to make this work later this week.

[Emily Riehl]

In the meanwhile, for tonight's class I made a BooleanWorld but it's pretty badly behaved.

Specifically, a lot of proofs require cases on a boolean b : B. But you can't see which case you are in while in typewriter mode (i.e., where the case b := false or b := true). Sometimes you can see his in editor mode but sometimes you can't. Eg, we could see the case when defining negation (cases on a single boolean) but not for conjunction (cases on two booleans).

[Emily Riehl]

There was another issue I encountered on the backend. I was trying to construct some sort of exercise involving a conjunction normal form which involved writing a bunch of iterated ands and ors. My level was supposed to be like

(p || !q || r) && (q || !r) && (!p || r) = something

but it seemed that the expression on the left-hand side was badly behaved (defined using a bunch of decides so wouldn't reduce to a truth value even when I was doing case splits on all the boolean variables).

When I rewrote the expression more laboriously in the form of (eg, this is something different):

and (and (and p (not p)) q) (not q)

it would reduce correctly after case splitting. Any idea what might be going on?

[Aaron Liu]

Emily Riehl said:

There was another issue I encountered on the backend. I was trying to construct some sort of exercise involving a conjunction normal form which involved writing a bunch of iterated ands and ors. My level was supposed to be like

(p || !q || r) && (q || !r) && (!p || r) = something

but it seemed that the expression on the left-hand side was badly behaved (defined using a bunch of decides so wouldn't reduce to a truth value even when I was doing case splits on all the boolean variables).

When I rewrote the expression more laboriously in the form of (eg, this is something different):

and (and (and p (not p)) q) (not q)

it would reduce correctly after case splitting. Any idea what might be going on?

what was the bunch of decides that were?

[Emily Riehl]

I'm on my phone so can't illustrate but I did a case split to turn all the variables into booleans. Then I was expecting the goal state to reduce to something that could be solved with rfl. This is what happened when I used "and" but not "&&".

[Emily Riehl]

Aaron Liu said:

Emily Riehl said:

There was another issue I encountered on the backend. I was trying to construct some sort of exercise involving a conjunction normal form which involved writing a bunch of iterated ands and ors. My level was supposed to be like

(p || !q || r) && (q || !r) && (!p || r) = something

but it seemed that the expression on the left-hand side was badly behaved (defined using a bunch of decides so wouldn't reduce to a truth value even when I was doing case splits on all the boolean variables).

When I rewrote the expression more laboriously in the form of (eg, this is something different):

and (and (and p (not p)) q) (not q)

it would reduce correctly after case splitting. Any idea what might be going on?

what was the bunch of decides that were?

@Aaron Liu here's another weird instance.

/-- There is some boolean `b` so that `b && b = b || b` -/
Statement : ∃ b : Bool, and b b = or b b := by
  exists false

gives no goals while

/-- There is some boolean `b` so that `b && b = b || b` -/
Statement : ∃ b : Bool, b && b = b || b := by
  exists false

gives

unsolved goals
⊢ (false && decide (false = false) || false) = true

[Emily Riehl]

Jon Eugster said:

We have the following Lean file somewhere in Robo where it is imported by Game/Metadata.lean. (import fconstructor from mathlib and overwrite constructor to use fconstructor instead)

modifided constructor from Robo

import Mathlib.Tactic.ExtendDoc
import Mathlib.Tactic.Constructor

open Lean Meta Elab Tactic

namespace Game

@[inherit_doc Lean.Parser.Tactic.constructor]
macro (name := constructor) "constructor" : tactic =>
  `(tactic| fconstructor)

extend_docs Game.constructor after "The variant used in the Robo game is called
`fconstructor` in Mathlib. The only difference is the real `constructor` sorts
the goals in a way not ideal for the game."

Thanks @Jon Eugster. I was able to use this to get the first equivalence level working!

In general, is there a way to tell which tactics the Lean game server knows about and which need to be imported.

In creating the backend of my first file about the existential quantifier, I find that I can use exists to solve the level (but then I'm not allowed to add it to the tactic list). I can add use (which I think I might prefer anyway) to the tactic list but I can't use it on the backend to solve the level.

import Game.Metadata

World "QuantifierWorld"
Level 6

Title "Introducing Existence"

Introduction "Let `P : A → Prop` be a predicate over a type `A`.

To prove the proposition `∃ x : A, P x` it suffices to find any element `a : A` so that `P a` holds.

Recall the function `and : Bool → Bool → Bool` capturing the logical notion of conjunction. Lean uses alternate notation `x && y = and x y`.

Recall also the function `or : Bool → Bool → Bool` capturing the logical notion of disjunction. Lean uses the alternate notation `x || y = or x y`

In this level, you are asked to prove that there exists some boolean `b : B` so that `b && b = b || b`.

The tactic `exists` is used to introduce proves of existentially quantified predicates.
"

/-- There is some boolean `b` so that `b && b = b || b` -/
Statement : ∃ b : Bool, (b && b) = (b || b) := by
  Hint "Type `exists` followed by the name of an element of `Bool` that you believe will satisfy the predicate. In some cases, such as this one, Lean will automatically be able to fill in the rest of the proof."
  exists false

Conclusion "The next level will give more practice with the existential quantifier. "

NewTactic use

[Dan Velleman]

It looks to me like Lean interpreted b && b = b || b as (b && (b = b)) || b, whereas I think what you wanted was (b && b) = (b || b)

[Emily Riehl]

Ah! Just a parenthesis error then. Thanks for diagnosing my weird error.

[Aaron Liu]

Emily Riehl said:

Aaron Liu said:

Emily Riehl said:

There was another issue I encountered on the backend. I was trying to construct some sort of exercise involving a conjunction normal form which involved writing a bunch of iterated ands and ors. My level was supposed to be like

(p || !q || r) && (q || !r) && (!p || r) = something

but it seemed that the expression on the left-hand side was badly behaved (defined using a bunch of decides so wouldn't reduce to a truth value even when I was doing case splits on all the boolean variables).

When I rewrote the expression more laboriously in the form of (eg, this is something different):

and (and (and p (not p)) q) (not q)

it would reduce correctly after case splitting. Any idea what might be going on?

what was the bunch of decides that were?

Aaron Liu here's another weird instance.

/-- There is some boolean `b` so that `b && b = b || b` -/
Statement : ∃ b : Bool, and b b = or b b := by
  exists false

gives no goals while

/-- There is some boolean `b` so that `b && b = b || b` -/
Statement : ∃ b : Bool, b && b = b || b := by
  exists false

gives

unsolved goals
⊢ (false && decide (false = false) || false) = true

I will investigate

[Emily Riehl]

@Aaron Liu this was a silly error that @Dan Velleman just caught. So don't waste time on it!

[Aaron Liu]

I figured it out

[Aaron Liu]

It's the parsing

[Aaron Liu]

Dan Velleman said:

It looks to me like Lean interpreted b && b = b || b as (b && (b = b)) || b, whereas I think what you wanted was (b && b) = (b || b)

Exactly this

[Kevin Buzzard]

That is quite a dubious precendence choice as far as I can see! From Init/Notation.lean in core Lean:

@[inherit_doc] infixl:35 " && " => and
@[inherit_doc] infixl:30 " || " => or

and

@[inherit_doc] infix:50 " = "  => Eq

and

@[inherit_doc] infixl:65 " + "   => HAdd.hAdd
@[inherit_doc] infixl:65 " - "   => HSub.hSub
@[inherit_doc] infixl:70 " * "   => HMul.hMul
@[inherit_doc] infixl:70 " / "   => HDiv.hDiv

so this seems to say "equality behaves how you'd expect when you're doing arithmetic" (because the arithmetic precedence numbers are bigger than 50) "...but not how you'd expect when you're manipulating booleans" (because the numbers are less than 50, so = will be greedy, which is what caused the problem). Do the boolean people not use = somehow?

Regarding

Emily Riehl said:

In general, is there a way to tell which tactics the Lean game server knows about and which need to be imported.

I think in NNG I would just import everything, and then develop, and then try to minimise imports afterwards. I also do this when writing FLT, sometimes things don't work because I didn't import Mathlib so I often import Mathlib when writing code, and then I have something in CI which stops me from merging any files with import Mathlib in (because then doc-gen generates all mathlib documentation for all of mathlib which makes CI really really slow) and I #min_imports to get the imports back down to a reasonable size (although this might not work with tactics, you might have to click on them to see what you need to import). Maybe import Mathlib.Tactic.Basic is a happy medium here? And probably it won't make CI run forever either, because I don't think doc-gen generates pages for tactics.

[Aaron Liu]

I think the precedence is just wrong

[Aaron Liu]

wrong for math

[Aaron Liu]

for programming maybe I can see an argument (but why not use BEq instead?)

[Siddhartha Gadgil]

The precedence looks correct to me. The expression x = 3 && y = 2 * x should be read as "x is 3" and "y is 2 times x". Usually && and || connect logical clauses and equality is within clauses.

[Aaron Liu]

I would agree if that said x == 3 && y == 2 * x

[Aaron Liu]

But this elaborates to some nasty expression full of decides

[Siddhartha Gadgil]

Aaron Liu said:

I would agree if that said x == 3 && y == 2 * x

Agreed. Either that or x = 3 ∧ y = 2 * x. The one I wrote mixes up Prop and Bool in a bad way.
But by the same token the expressions that gave the error should also have == if they intend to be part of Boolean arithmetic.

[Aaron Liu]

I feel like x == 3 && x == 4 = false parses pretty unambiguously (but maybe you disagree?)

[Emily Riehl]

I'm back with another weird thing I'd like to do with a Lean game.

I'm in the process of building a natural numbers world, which is meant to just contain a few levels explaining how the natural numbers work in dependent type theory, rather than replicate the whole natural numbers game. I stole the custom induction tactic from the nng4 library (because I was confused by some of the outputs of the vanilla induction n) but unlike the natural numbers game, I'm using mathlib's Nat rather than a custom defined natural numbers.

[Emily Riehl]

What I was hoping to do, though, is talk about both induction (proving propositions) and recursion (defining functions out of Nat). A very simple case would be the predecessor function which we could use to show that successor is injective. @Jon Eugster or anyone do you think it would be possible to do this in a Lean game?

[Emily Riehl]

Using the custom induction tactic (which I don't understand) I can define this

/-- There is a function `pred : Nat → Nat` that sends `0` to `0` and `succ n` to `n`. -/
Statement : Nat → Nat := by
  intro n
  induction n with k
  exact 0
  exact k

but I have no idea if this is the right function because I don't understand what is happening in the successor case. When my cursor is at the start of the final line, the infoview shows

case succ
k a : Nat
⊢ Nat

I have no idea what a is here. If I write induction n with k hk then a becomes hk so it's the name for the inductive hypothesis, I guess, but what is that?

I've also tried

/-- There is a function `pred : Nat → Nat` that sends `0` to `0` and `succ n` to `n`. -/
Statement : Nat → Nat := by
  intro n
  cases n
  exact 0
  exact n_1

and at the start of the last line the infoview shows

case succ
n_1 : Nat
⊢ Nat

Again I don't know if I should interpret this as defining the value of the function on succ n_1 or something else...

[Aaron Liu]

the induction hypothesis is the previous result

[Aaron Liu]

so if you're defining a function f n by cases on n then in the zero case you define f 0 and in the successor case you have a number k and the induction hypothesis hk = f k and you want to define f (k + 1)

[Emily Riehl]

Is there any way to make this more clear in the infoview?

[Aaron Liu]

I can't think of how that would work

[Aaron Liu]

generally you don't use tactics to construct data like this so

[Emily Riehl]

Yeah, I know I'm being weird. I wasn't sure the game infrastructure would work with the usual syntax of something like:

| 0 => 0
| succ n => n

[Emily Riehl]

A more basic question: I'm starting each level with open Nat to give me direct access to eg add_succ. I don't know how to get the ℕ notation without breaking everything.

[Aaron Liu]

what are your imports

[Aaron Liu]

have you imported docs#termℕ

[Emily Riehl]

I haven't the slightest idea what's being imported tbh. But I just added that code in a file in the metadata directory and imported that and now it works. So thanks!

[Jon Eugster]

Indeed, the \N notation is in mathlib not in Lean itself, so one needs to import that file from mathlib or copy-paste the notation:+1:

generally, having a level which is just Nat -> Nat might be a bit pointless as a student can define any function to solve the level. You probably want a level which says something like `\exists f : Nat -> Nat, [some condition about f]

about the induction hyp a : Nat := f k, does it show the := f k with the regular induction in the normal infoview, or does it not show that either? If it's just about the bug which doesn't display def values in-game, I'm hoping to fix that very soon

[Aaron Liu]

it's not a def at that point yet since you're still defining it

[Aaron Liu]

it's like a list foldr, you have a base case and a folding function which takes as input the value of the list at the current location and also the previous output of the foldr

[Aaron Liu]

Nat is just like a list but it doesn't hold any values (so like a List Unit)

[Aaron Liu]

and the recursion is like the list foldr

[Aaron Liu]

so when you're writing your folding function that previous value you take as input doesn't have a definition

[Jon Eugster]

that makes sense

[Jon Eugster]

NNG's induction is really just a copy of mathlib's induction' so I guess mathlib's cases' would be the deaired tactic here, which would accept cases' n with k. Not sure if NNG already has this or if it would nees to be copied from mathlib

[Jon Eugster]

Here's a fun idea for a level:

import Mathlib.Tactic.Common

Statement (preamble :=  let f : Nat -> Nat := ?_; use f; swap) : ∃ f : Nat -> Nat, f 0 = 0 := by
  sorry
  sorry

That should give you a level with two goals. in goal 1 you habe to define a function and in goal 2 you prove a property about the defined function

[Emily Riehl]

I like the idea of having the level be both to define a function and to prove a property about it. I was experimenting with one about the closed form for the triangle numbers but then gave up because I couldn't get it to work.

What does this do (preamble := let f : Nat -> Nat := ?_; use f; swap) in the code block above?

[Emily Riehl]

For those following along, the levels of my (preliminary) natural numbers world can be found here. These use induction' rather than cases' which I didn't have time to experiment with.

From a user experience perspective, the recursion level in particular is not so great. The info view gives no information about what the objective is or how to interpret the variables in the context.

My students also experienced some weird glitches with adding successors and commutativity of addition. Some were able to rw [add_succ] but others had to rw [Nat.add_succ] and I have no idea why.

[Jon Eugster]

Emily Riehl said:

What does this do (preamble := let f : Nat -> Nat := ?_; use f; swap) in the code block above?

Inside the preamble argument goes any tactic sequence which is then executed directly after the by and before the player's code.

So you want to put a tactic sequence there which turns the statement into the goal you want to show to the player. My aproach here was that ?_ creates an additional goal to fill in later, but it got added as last goal, so I used swap to make the player define the function before proving something about it.

That's similar to the constructor vs fconstructor, Lean likes to put auxiliary goals at the end and work with metavariables ?f which it usually fills automatically eventually, but in the game you usually want the reversed order as people should define all the stuff manually first.

[Jon Eugster]

Emily Riehl said:

From a user experience perspective, the recursion level in particular is not so great. The info view gives no information about what the objective is or how to interpret the variables in the context.

I'll try to fix this today and tomorrow, @Alex Kontorovich has also been plagued by this annoying bug

[Jon Eugster]

Emily Riehl said:

Some were able to rw [add_succ] but others had to rw [Nat.add_succ] and I have no idea why.

Make sure all levels have

open Nat

in their file. Otherwise my guess is that mathlib might have a _root_.add_succ which might have been used instead of Nat.add_succ and that might have caused unexpected behaviour. But that's just a wild guess, haven't looked at the code.

[Alex Kontorovich]

Jon Eugster said:

Emily Riehl said:

From a user experience perspective, the recursion level in particular is not so great. The info view gives no information about what the objective is or how to interpret the variables in the context.

I'll try to fix this today and tomorrow, Alex Kontorovich has also been plagued by this annoying bug

What I've suggested to my students is to give themselves API, the same way we do in Mathlib! E.g., if you define $f(x)=x^2$, also give yourself a have that you can rewrite by:

let f x := x^2
have f_is (x) : f x = x^2 := by rfl

That's a pretty easy workaround for the "bug"...

[Emily Riehl]

I'm not entirely sure I understand. @Alex Kontorovich can you point me to a level in your game where you do something like this?

My issue is that a level has a goal of defining, e.g., the sequence of triangular numbers. So the goal is of type Nat -> Nat and after they type intro n; induction n all they see is a goal of type Nat without a reminder that what they are supposed to be doing is defining the 0th triangular number, and similarly for the recursive step.

[Emily Riehl]

Also this fails:

/-- There is a function `pred : ℕ → ℕ` that sends `0` to `0` and `succ n` to `n`. -/
Statement (preamble :=  let f : Nat -> Nat := ?_; use f; swap) : ∃ f : ℕ → ℕ, (f 0 = 0) ∧ (∀ n : ℕ, f (succ n) = n) := by

I have a read underline under the semicolon before swap with error message

unexpected token ';'; expected ')'

When I remove that and the swap I get the goals in the wrong order.

Note I'm using a custom constructor redefined to be fconstructor so perhaps I don't need this preamble?

[Aaron Liu]

Maybe you need more parentheses

[Aaron Liu]

Try putting parentheses around the entire tactic, so like
(preamble := (let f : Nat -> Nat := ?_; use f; swap))

[Alex Kontorovich]

Hi Emily, maybe it would be easier to show you what I have in mind over a quick zoom call? Feel free to send a DM with your availability. Best, Alex

[Emily Riehl]

@Alex Kontorovich I remember why I don't have the let tactic in my library. When I try NewTactic "let" I get a weird error. But you have it in your game. How did you manage this?

[Alex Kontorovich]

Oh yes, I learned this the hard way! You have to use "French quotes":

/-- The `let` tactic is like `have`, but for creating variable names or functions. -/
TacticDoc «let»

NewTactic «let»

In my game, it appears for the first time in Lecture 10 Level 4, in case that's helpful...

[Emily Riehl]

Jon Eugster said:

Here's a fun idea for a level:

import Mathlib.Tactic.Common

Statement (preamble :=  let f : Nat -> Nat := ?_; use f; swap) : ∃ f : Nat -> Nat, f 0 = 0 := by
  sorry
  sorry

That should give you a level with two goals. in goal 1 you habe to define a function and in goal 2 you prove a property about the defined function

@Jon Eugster has been helping me make some levels in Boolean world of my dependent type theory game that ask students to define particular functions Bool -> Bool prior to introducing existential quantifiers.

I was hoping to use a similar trick for the boss level which ask them to solve a CNF problem, but the tactics don't quite work. In the source code

import Game.Metadata

World "BooleanWorld"
Level 9

Title "Boss Level"

Introduction "
An expression involving booleans is in *conjuctive normal form* if it expressed as a conjunction (possibly involving many formulas) of disjunctions (possibly involving many formulas) of either booleans or their negations.

Using Lean's alternate notation for conjunction, disjunction, and negation, conjunctive normal form statements look like

`(p || !q || r) && (q || !r) && (!p || r)`

For the Boss Level, you are asked to find booleans `p q r : Bool` so that

`(!p || q) && (!q || p) && (!p || !r) && (!q || !r) && (p || q)`

is satisfiable, meaning that the after substituting appropriate elements for `p q r`, this conjunctive normal form formula is equal to `true`.

Solve the first three goals by `exact p`, `exact q`, and `exact r` — replacing the boolean variables by explicit booleans `true` or `false` as appropriate. If you have found the right solution, the final goal should be solvable with `rfl`.
"

/-- The following expression in conjunctive normal form is satisfiable. -/
Statement (preamble := let p : Bool := ?_; let q : Bool := ?_; let r : Bool := ?_) : ∃ p : Bool, ∃ q : Bool, ∃ r : Bool,
and (not p || q)
(and (not q || p)
(and (not p || not r)
(and (not q || not r)
(p || q)))) = true := by
  Hint "For this level to work, we need to swap the goals. Type `pick_goal 4` to move the fourth goal to the front."
  pick_goal 4
  Hint "Now supply your conjectured value of `p` with `exact ??`."
  exact true
  Hint "Now type `pick_goal 3` to move the third goal to the front."
  pick_goal 3
  Hint "Now supply your conjectured value of `q` with `exact ??`."
  exact true
  Hint "Now type `pick_goal 2` to move the third goal to the front."
  pick_goal 2
  Hint "Now supply your conjectured value of `r` with `exact ??`."
  exact false
  Hint "Now type ⟨p, q, r, rfl⟩` to use these values and attempt to solve the goal by `rfl`. If this works, congratulations! If not, go back and change the values for `p`, `q`, and `r`. Ignore the funny looking `∃` symbol in the formula, which will be explained in a future world."
  exact ⟨p, q, r, rfl⟩

Conclusion "If this was too easy, you might find it interesting to learn that the general problem of identifying whether a formula in conjunctive normal form is satisfiable is NP complete!"

/-- `pick_goal n` will move the `n`-th goal to the front. -/
TacticDoc pick_goal

NewTactic pick_goal

you can see what I'm trying to do. But I'd like to move the goal swapping tactics and the use stuff into the preamble so the user would solve the four goals with exact true; exact true; exact false; rfl. Is this possible?

[Aaron Liu]

did you try the goal swapping tactics

[Emily Riehl]

So swap doesn't seem to work since I need a more complicated permutation.

[Aaron Liu]

I can immediately think of swap, rotate_left, rotate_right

[Aaron Liu]

oh and there's also pick_goal

[Emily Riehl]

Yeah you can see that's what I'm using to solve the level but I want it in the preamble. This compiles

/-- The following expression in conjunctive normal form is satisfiable. -/
Statement (preamble := let p : Bool := ?_; let q : Bool := ?_; let r : Bool := ?_; pick_goal 4; pick_goal 4; pick_goal 4) : ∃ p : Bool, ∃ q : Bool, ∃ r : Bool,
and (not p || q)
(and (not q || p)
(and (not p || not r)
(and (not q || not r)
(p || q)))) = true := by
  Hint "For this level to work, we need to swap the goals. Type `pick_goal 4` to move the fourth goal to the front."
  -- pick_goal 4
  Hint "Now supply your conjectured value of `p` with `exact ??`."
  exact true
  Hint "Now type `pick_goal 3` to move the third goal to the front."
  -- pick_goal 3
  Hint "Now supply your conjectured value of `q` with `exact ??`."
  exact true
  Hint "Now type `pick_goal 2` to move the third goal to the front."
  -- pick_goal 2
  Hint "Now supply your conjectured value of `r` with `exact ??`."
  exact false
  Hint "Now type ⟨p, q, r, rfl⟩` to use these values and attempt to solve the goal by `rfl`. If this works, congratulations! If not, go back and change the values for `p`, `q`, and `r`. Ignore the funny looking `∃` symbol in the formula, which will be explained in a future world."
  rfl

but it doesn't actually seem to treat the cases in the order I want (p then q then r). When I mouse-over the preamble it looks like that order but when I fill in the values it assigns false to p which is wrong.

[Aaron Liu]

what order do they end up going in

[Aaron Liu]

can you pick_goals in a different order to order it correctly?

[Emily Riehl]

r, q, p

[Emily Riehl]

What's weird is in the infoview it looks like I'm doing it right. I've tried replacing all three pick_goal 4s with rotate_right to the same result. Also at the end I need exact <p,q,r,rfl> instead of just rfl.

[Aaron Liu]

oh

[Aaron Liu]

well then why not just start with refine ⟨?p, ?q, ?r, ?eq⟩ instead of all those lets

[Emily Riehl]

Thanks. This works. (Though when I tried implementing it for the earlier levels 1, 3, 5 it made the infoview into something a bit less informative for reasons I don't understand.)

[Emily Riehl]

But for this level it's much cleaner.

[Jon Eugster]

You might have figured this out already, but I noticed you get much better error messages when you first develop your proof normal (i.e. as single lines after := by) and only once it's working you start moving the first couple lines into the (preamble := .... ) argument.;-separated.

It looks like parsing is less forgiving inside the argument so you get weirder error messages if something is wrong. (maybe that's because I defined the syntax with the wrong priority or something, haven't checked)

[Jon Eugster]

note that refine ⟨?p, ?q, ?r, ?eq⟩ is short for refine ⟨?p, ⟨?q, ⟨?r, ?eq⟩⟩⟩ where each parenthesis represents one existential quantifier. that seems to be a nice approach and Im surprised it doesn't work alike for your previous levels

[Emily Riehl]

The refine works for eg boolean world level 1 (negation). But when I do the longer preamble with preamble := let f: Bool → Bool := ?_; use f; swap I get the following at the start of the second goal:

Screenshot 2025-10-28 at 11.25.39 AM.png

[Emily Riehl]

Whereas if I do the preamble := refine <?f, ?eq> preamble the start of the second goal looks like this:
Screenshot 2025-10-28 at 11.29.54 AM.png

[Emily Riehl]

I think the former is easier to read.

[Aaron Liu]

then you can refine let f := ?f; ⟨f, ?eq⟩ instead

[Emily Riehl]

That's perfect. Much cleaner from the user side. Thanks for helping me sort this out both of you!

[Gihan Marasingha]

I'm having problems installing the lean4game. When running npm install on my local machine, I get the message

npm error code E402
npm error 402 Payment Required - GET https://gitpkg.vercel.app/hhu-adam/lean4monaco/esbuild-import-meta-url-plugin?main

Similar errors appear when trying to build a container in GitHub Codespaces.

@Jon Eugster

[Julian Berman]

It looks like that service (gitpkg) hasn't paid its Vercel bill and might be gone for good?
The reason it exists seems to be to support installing straight out of git repos when your package lives in a monorepo / in a subdirectory. I don't actually see an alternative to that that isn't "upload those 2 deps to NPM" or "vendor them as subrepos/submodules" that works, though I'm no JS dev.

[Jon Eugster]

Thanks for letting me know. I'll probably look at that - together with the latest Lean version bump - on Sunday

[Snir Broshi]

https://github.com/ramasilveyra/gitpkg/issues/68

The readme for lean4monaco says "This could be replaced by npm install --save-dev @codingame/esbuild-import-meta-url-plugin when this PR is accepted", and that PR has been accepted (as a separate commit), so maybe lean4game can just switch over.

Of course then you'll discover that the lean4-infoview is also specified using a gitpkg url, which points to version 0.4.2 of @leanprover/infoview, but I think it has to use gitpkg because the dependencies also specify "@leanprover/infoview": "^0.4.3" so this allows for 2 different versions to be installed.

[Emily Riehl]

I've just tried to update my Lean game for the first time in a few months and the usual import trigger does not seem to be having any effect. Do I just need to be more patient or is there some issue? In case it's relevant the game is here.

[Alex Kontorovich]

I had the same issue; Jon will update a token tonight, and the trigger mechanism should work tomorrow...

[Jon Eugster]

I've updated all access tokens and triggered reimporting for both your games now :)

[Emily Riehl]

Would it be possible to add a DisabledDefinition to parallel the current DisabledTheorem? Eg Product World Level 6 can be solved with exact Function.curry and it would be great to disable this!

[Alex Kontorovich]

I'm confused, you're adding Function.curry to the game right at that level? You could just postpone its availability to the next level, no? You could say in the Introduction something like "after this level, you'll be able to write exact Function.curry, but here you'll need to prove the theorem on your own", something like that? Then move the DefinitionDoc/NewDefinition to Level 7... Would that accomplish what you want?

[Emily Riehl]

I'm maybe handling the library for both theorems and definitions in a stupid way.

I was despairing of the prospects of manually importing each file into all of the subsequent files to make the theorems proven there available later. So both the theorems and definitions in the library are things that are coming from mathlib. How exactly they are being imported into the game is a bit of a mystery to me.

In particular, I'm not including the construction produced in every single level. (For example, I don't know the mathlib name for the theorem P ∧ Q → P ∨ Q from level 2 of disjunction world.)

In any case, I've been advised by @Jon Eugster that since several of my levels ask the player to define an element of a type rather than prove a theorem it's better practice to use external definitions rather than user supplied ones.

[Emily Riehl]

On another point, I have a build error right now on my game repository that I don't understand:

Run : Get Mathlib Cache
Mathlib Cache
  /home/runner/work/_temp/e0195d82-b36b-4f64-b399-015e5347315d.sh: line 3: lake: command not found

Did I do something wrong and if so how do I fix it?

[Snir Broshi]

Emily Riehl said:

Did I do something wrong and if so how do I fix it?

No, GitHub is whack right now, see https://www.githubstatus.com/incidents/xntfc1fz5rfb and #rss > GitHub Status - Incident History
Mathlib's master doesn't even build
(also a bit related - https://www.youtube.com/watch?v=E3_95BZYIVs)

[Snir Broshi]

Oh they posted 15 minutes ago that things are back to normal

[Snir Broshi]

Tested myself, it's not fixed, GitHub Actions is still the worst

[Emily Riehl]

Just tried a rerun which gave me a new message

 ✖ [2/2] Running proofwidgets:release
  error: failed to fetch GitHub release (run with '-v' for details)
  error: build failed
  Some required targets logged failures:
  - proofwidgets:release
  uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1

[Snir Broshi]

Some Mathlib PRs are failing but some are succeeding, I think it's random, probably based on which runner you get

[Jon Eugster]

Emily Riehl said:

Would it be possible to add a DisabledDefinition to parallel the current DisabledTheorem? Eg Product World Level 6 can be solved with exact Function.curry and it would be great to disable this!

Currently the game isn't restricting which definitions are allowed in a proof (only tactics and theorems are checked). But I think there should be no obstactle to inplementing that..

[Jon Eugster]

(deleted)

[Prakriti]

I've been seeing this error in the typewriter mode of the game since yesterday when I run my game: Crashed! Go to editor mode and fix your proof! Last server response: And in the console logs, I can only see the following error: Cannot process request to closed file '.../Game/Metadata.lean'. I could not find any helpful information so far to solve this issue.

Has anyone ever encountered this error and could help me understand what exactly is going on?

[Snir Broshi]

Just to check: are you unable to play your game at all or does this only happen when you resize the window?

[Prakriti]

I'm not able to play my game at all. Also, currently I'm not able to run my game locally because of this issue. So I decided to go on with this suggestion.

[Jon Eugster]

Prakriti said:

I've been seeing this error in the typewriter mode of the game since yesterday when I run my game: Crashed! Go to editor mode and fix your proof! Last server response: And in the console logs, I can only see the following error: Cannot process request to closed file '.../Game/Metadata.lean'. I could not find any helpful information so far to solve this issue.

Has anyone ever encountered this error and could help me understand what exactly is going on?

Could you create a github issue providing a bit more information about which game you are playing, whether this is on the server or a local instance and maybe also which OS/browser you're playing from. Maybe also the concrete level and the code you've entered so far (i.e. toggle to editor mode and copy-paste all the lines of code)

I'll try to look at that issue this week