We made a board game for LEAN

Stream: Lean for teaching

[Yuntian Liu]

Hello, I'm new to the Lean Zulip community, but I've been studying Lean and working on AI4Math research for a while. I'm a leading member of Shanghai Jiao Tong University (School of Mathematical Science) AI4Math team, and we have been trying to make academical contributions to the territory, though no papers have been officially published yet. Several months ago, our team decided to host a summer school course, which started this morning, to attract more interested people to learn and use Lean.
1.jpg
(Picture of me teaching what a tactic proof is)
I designed a board game based on the mechanisms of tactic proof, as shown in the photos below. The original intention was to help the beginners memorize the tactics quickly to prove propositions of logical operators. But since I posted a photo of our team testing the game in a chat group, many people have shown great interest and would like to get the cards or the design.
The problem is, making these customized cards costs a lot of money, and is simply beyond the budget of our team to give them out for free. Also we never intend to make a profit with the game, and I fear there might be copyright problems.
I believe the idea is so great, and has the potential to attract many who still don't know or aren't interested in Lean, especially kids or Math beginners, to learn about Lean and join the community and make contributions, so I want to make the game accessible to everyone around the world. But I don't want to distribute my original card design all around and get pirated by some company starting to make money out of it. So I wonder if there are any possible ways that the design of the game gets support from the Lean developers officially, and gets a better way for people around the world to access it, either for fun or to inspire kids about formal mathematics.
I sincerely look forward to your help, community members, thank you.
2.jpg
3.jpg
4.jpg

[Eric Wieser]

I suppose one option would be to try to make a virtual version using Board Game Arena

[Yuntian Liu]

Eric Wieser said:

I suppose one option would be to try to make a virtual version using Board Game Arena

Okay, we will try to develop one later.
But still I want people to get tangible cards, since playing video games deprives part of the fun playing real cards. I wonder if some kind of official repository can be set up for people to download the design and make their own cards?

[Malvin Gattinger]

If you make the design public but do not want anyone else to make money from it, maybe consider putting it under a Creative Commons "NC" license that only allows non-commercial use? (Assuming the cards do not contain anything that you are not allowed to put under that license. And I am not a lawyer etc.)

[Joachim Breitner]

Nice board game!

I'm not sure I fully understand your worries about copyright issues. Are you worried that you are infringing someone else's copyright, or that someone else “steals” your work?

If it's the latter, I suggest to not worry. Maybe unfortunately, but I don't think the market for lean themed board games is commercially attractive yet :sweat_smile:.

If you want to share, I'd say just put them online (e.g. A GitHub repo), maybe put a CC license on it, and cherish if someone uses it. All of Lean is distributed that way!

[Kevin Buzzard]

What are the rules?

[Joachim Breitner]

Whatever they are, I'm sure they are macro_rules :-)