Convert GlimpseOfLean into Lean Games for Beginners

[RexWzh]

Hi everyone,

This is Rex, and I have been exploring this fantastic project. It's a great starting point for newcomers to get an introduction to Lean! And I think it could be even more engaging and accessible for beginners, if we transform it into a Lean4Game project.

This approach would eliminate the need to configure the VS Code environment or use GitHub/Gitpod codespace, making it much easier and more enjoyable for new users to dive into Lean.

Current progress:

I've made some initial efforts to set up this project, https://github.com/Lean-zh/GlimpseToGame. However, I encountered errors related to the mathlib compatibility. For more details:

• Failed to Configure mathlib Dependency for GlimpseOfLean in lean4game leanprover-community/lean4game#256 .

The core issue stems from the fact that Lean4Game currently supports mathlib up to version 4.7.0, while mathlib 4.8.0 support is still a work in progress as noted here

• Update to Lean v4.8 leanprover-community/lean4game#243

Request for help:

To move forward, it would be helpful if GlimpseOfLean could be made compatible with mathlib version 4.7.0. or create a new branch base on 4.7.0. This requires some modifications to the GlimpseOfLean/Library/Basic.lean file. Since I'm still in the process of learning Lean4, I'm not entirely confident in making these changes myself.

Would anyone be able to assist with updating the necessary files or provide guidance on how to achieve this compatibility? Your help would be immensely appreciated!

Thanks in advance for your support and consideration.

[joneugster]

Im sorry I haven't been able to put updating lean4game on my priority list yet :(

[joneugster]

If you dont want to bother with the incompatiblility, you could set up your game without importing lean4game.

Still create one file per level, just use example or theorem and not the Statement. Write the text just as comments.

That way you could get the game almost finished without depending on v4.7 and once I've got my shit together, it should be basically a quick (semi-)automatic replacement to turn your project into a game.

[RexWzh]

Hi @joneugster

I’m sorry if my previous messages came across as pushy – that was not my intention at all. Lean4Game is one of the most interesting Lean projects I've met. Its potential to make Lean accessible to mathematicians with minimal programming skills is incredibly exciting. I'm eager to contribute to Lean4Game, though my contributions have been limited to small PRs for non-lean-code improvements so far.

My background lies in pure mathematics, and I'm currently learning Lean4 through Theorem Proving in Lean. I hope to assist with fixing compatibility issues in the future.

Learning while creating projects can be quite rewarding, and I believe that GlimpseOfLean could serve as a starting point.