Reintroduction to Proofs on the Lean Game Server

Stream: new members

[Emily Riehl]

I'm proud to report that a game I developed while teaching a first year seminar course at Johns Hopkins this past fall has now joined the featured games list on the Lean Game Server.

In a talk called A reintroduction to proofs, I've speculated about teaching an undergraduate level introduction to proofs course but using dependent type theory as the implicit formal system in place of set theory and first order logic.

The Reintroduction to Proofs Game does just this, using Lean tactics to animate the analogy between function types and implications, product types and conjunctions and so on. Following a suggestion made by @Kevin Buzzard this past summer, there is a world studying constructions involving the empty type before introducing negations, which allows us to separate out constructive proofs (eg double negation introduction) from classical ones (such as double negation elimination).

This was made possible by the good folks who built the Lean Game Skeleton repository and answered questions on the Lean for teaching thread, such as @Alex Kontorovich, @Aaron Liu, and @Dan Velleman. In particular, @Jon Eugster saved me several times, when I needed help in a rush before my text class.

After the semester ended, I reordered several of the worlds and made various edits and additions. Further contributions are very welcome, especially in the form of PRs to this repository.

[Emily Riehl]

For those who want to contribute, here are some things I know could use more attention:

1. The library, which is a bit weirdly structured. Most of the stuff that's included as definitions or theorems actually comes from mathlib, rather than theorems proven in the levels (the exception being most of Advanced Function World). Was this the right call? I'm not sure. On the one hand, it seemed nicer to avoid clutter of stuff that isn't necessary. But it could certainly be made more robust and be better structured.
2. The Boss Levels are a bit uneven. A few are really great, like the Boss Level of Function World. But others are either boring or a bit too easy. Suggestions would be very welcome.
3. The final Dependent World is a bit stubby (written hastily at the very last minute). I'd love to include some better examples of dependent types over the booleans or the naturals, but I don't want to depart too much from how things are handled in Mathlib. I thought about including something like Fin but redefined to be an iterated coproduct of the the unit type and perhaps reindexed so that the type family has a section. But this felt a bit complicated so I left it out.

[Julian Berman]

This is awesome! Perhaps a very small suggestion (which can't be done via a PR otherwise I'd happily send one) is to add the link to play the game (i.e. https://adam.math.hhu.de/#/g/emilyriehl/reintroductiontoproofs) as the URL in your repository in GitHub so someone can get immediately to that page from the repo -- you can get there from the gear menu on github, i.e. on the right here:

Screenshot 2025-12-30 at 18.20.34.png

(and then entering that URL in the website field).

[Emily Riehl]

Thanks for explaining! (This would have never occurred to me.) Done :)

[Philippe Duchon]

This is really nice! For some reason, I get stuck on level 5/9 of Boolean world. Starting from the initial state (with a first goal of Bool -> Bool -> Bool) I tried various ways of defining my function (in ways that work in VSCode, either with a cases or a match, and even with a direct exact fun b1 b2...), but each time I end up with three goals: one is the original Bool -> Bool -> Bool, the second is the original second goal (with ?f in place of the or function), and the third is the second, only with ?f replaced by my definition of the or.

(Not sure how to explain this in understandable terms)

In my non-expert eyes, this looks like, behind the scene, Lean is in a state where it expects me to define a function, only it doesn't quite work in the expected way.

[Aaron Liu]

Can you paste the code you used?

[Philippe Duchon]

intro b1 b2
cases b1
exact b2
exact true

Alternatively:

intro b1 b2
exact (match b1 with | false => b2 | true => true)

Or:

exact fun b1 b2 => match b1 with | false => b2 | true => true

[Aaron Liu]

oh, this is the one I cheesed with exact fun a b => !(!a && !b)

[Aaron Liu]

I'm trying all three of your code snippets and they all leave me with the one goal of showing your f works:

Current Goal
Objects:
f : Bool → Bool → Bool := ⋯
Goal:
f true true = true ∧ f false true = true ∧ f true false = true ∧ f false false = false

[Philippe Duchon]

Well, your code does, but mine leaves me with the Bool->Bool->Bool goal. Maybe my game is in a strange state?

[Aaron Liu]

maybe a screenshot would be helpful?

[Philippe Duchon]

Here's one where the problem shows after I used your version of or: after starting the proof of correctness, the Bool->Bool->Bool goal shows up again.

Capture d’écran du 2025-12-31 23-53-55.png

[Aaron Liu]

oh

[Aaron Liu]

that's not what I thought you did

[Aaron Liu]

I'm a bit busy now, but I'll take a look later

[Jon Eugster]

I cant investigate, but the "strange state" Lean is in, is somehing like

def .... : Exists f, P f := by
  let f : Bool -> Bool -> Bool := ?_
  use f
  swap
  sorry -- definition
  sorry -- property

so the two goals in the two tabs are the ?_ and the second sorry.

Hope that helps figuring out what's happening

[Aaron Liu]

can't figure it out
image.png

[Jon Eugster]

maybe you could add the code (copy paste from editor mode) and a link to the level here:

https://github.com/leanprover-community/lean4game/issues/402

Might be related. Or at least that will be the issue I will have to look at first after the holidays.

[Alfredo Moreira-Rosa]

@Emily Riehl in many occasions the definitions are already unlocked allowing to bypass the construction of the proofs. exemple :
image.png

[Emily Riehl]

@Philippe Duchon this is very strange. I played exactly the way you did but after solving the intermediate goal (defining the function) I was left with just one further goal (the four equalities). Of course constructor then breaks it into multiple subgoals but none of these involved redefining the function.

Screenshot from 2026-01-01 13-31-27.png

[Emily Riehl]

So indeed this seems like some sort of bug. If you delete all your code and start again does it happen every time?

[Emily Riehl]

@Alfredo Moreira-Rosa thanks for pointing out a clear example of this. I discussed this sort of issue once with @Jon Eugster and I think this might require some development on the backend of the Lean game server. It allows for a command DisabledTheorem to disallow the use of certain theorems in a level but I don't think it currently supports anything like DisabledDefinition. But if I'm wrong or if this gets fixed, it would be good to cut off these shortcuts.

[Emily Riehl]

(Or maybe it's best for advanced users to allow them? I'm not sure...)

[Aaron Liu]

Emily Riehl said:

Alfredo Moreira-Rosa thanks for pointing out a clear example of this. I discussed this sort of issue once with Jon Eugster and I think this might require some development on the backend of the Lean game server. It allows for a command DisabledTheorem to disallow the use of certain theorems in a level but I don't think it currently supports anything like DisabledDefinition. But if I'm wrong or if this gets fixed, it would be good to cut off these shortcuts.

The DisabledDefinition command seems to be defined right after DisabledTheorem

[Philippe Duchon]

Emily Riehl said:

So indeed this seems like some sort of bug. If you delete all your code and start again does it happen every time?

Yesterday it still happened every time, even after I closed my browser and relaunched it. Today I tried again, and everything worked as I was expecting. I don't know how this all works server-side, but I suppose some sort of session was preserved and expired since yesterday? (I hope it's not just because of the new year, presumably it's just some forme of session expiring). My progress (and existing code on this level) was preserved.

[Jon Eugster]

Aaron Liu said:

The DisabledDefinition command seems to be defined right after DisabledTheorem

You're right, this has been implemented, just not documented :) @Emily Riehl

[Jon Eugster]

@Philippe Duchon your code is store client side (browser local storage).

Please add your observations to the bug issue, so I'll find it easily when looking at some lean4game-related things next week

[Philippe Duchon]

Hmm, I completed the full game, but I admit that for most of Dependent World (and a good part of Equivalence World), I was mostly going forward blindly, looking at what the goals were, seeing only one way to move forward, and crossing fingers hoping that rfl would solve the proof parts - which it did.

So I have absolutely no suggestions as to how to accomplish this, but I'd say a few more intermediate levels might make the player believe they actually learned something.

Still, the whole experience was pretty interesting!

[Michael Bucko]

The game is awesome. Thank you!

A side note: it looks like I experienced an issue in Boolean World, i.e. I completed it, then some of levels got marked gray (from green), and the last level of Quantifier World got unlocked. Also, even though the last level of Quantifier World is unlocked & solved, all the previous ones are marked gray.

Screenshot 2026-01-08 at 15.10.01.png

[Kevin Buzzard]

There's a switch on the home screen where you can change the "rules" and if there are no rules then you can do any level whether or not you've unlocked it. Did you perhaps do this level earlier?

[Michael Bucko]

Kevin, good point. I completed both Boolean World and Quantifier World, and then not only Boolean World got partially marked gray, but also all (but one) of the Quantifier World levels.

The "rules" switch is set to "regular".

[Michael Bucko]

Btw. didn't have to do Boolean World twice. Just opened the last challenge in Quantifier World, and then pressed "previous" a bunch of times (so I only had to do Quantifier World twice).

Screenshot 2026-01-08 at 22.49.27.png

[Michael Bucko]

For the reference, the same thing happened again. I completed the previous levels and then Advanced Function World (and some of the next levels), and then multiple levels got unmarked green (and marked gray).

Screenshot 2026-01-10 at 07.05.05.png

[Jon Eugster]

That sound like a bug...

The "completed"-flag for each level is stored in browser storage and recalculated when the level is opened, so it does make sense that clicking through the badly displayed levels would have an effect.

Even switching to ruleset "relaxed" an click on the level which is wrongly gray might recalculate it from the stored proof and mark it green.

If you are still in an erroneous state, could you download your progress (menu on this overview page) and send me that json please?

[Michael Bucko]

Thank you! It's working now. I just did the remaining Advanced Function World again, and should finish the entire game today.

[Michael Bucko]

It worked! The game is great.
Screenshot 2026-01-10 at 12.41.38.png

If I experience anything like this anymore (perhaps it's a very rare case), I'll look into the logs.