Set Theory Game

Stream: general

[Dan Velleman]

The set theory game is still under development--I'm planning to add two more worlds. Feedback/suggestions welcome!

[Shreyas Srinivas]

Could we have a corresponding thread in #general for this. I do have some suggestions.

[Brandon Brown]

Dan Velleman said:

The set theory game is still under development--I'm planning to add two more worlds. Feedback/suggestions welcome!

I just started it. I think from a didactic standpoint pointing out the functional nature is helpful. For example, $h : A \subset B$ is a function $x \in A \implies x \in B$, so if you applied this function to an $x \in A$ you get the $x \in B$.

[Notification Bot]

3 messages were moved here from #announce > Lean Game Server by Oliver Nash.

[Shreyas Srinivas]

Currently the game feels too focussed on apply and exact tactics. By the time one gets to the third world, it gets redundant. I was hoping that at least after the second world, there could be an interlude where some of the proofs are repeated, but with more powerful tactics (tauto, left, right, and ext come to mind), as well as cleaner ways to write proofs for multiple cases (i.e. case, cdot, | notation)

[Shreyas Srinivas]

On the one hand, repeating proofs with more powerful tactics after they have been done with simpler tactics helps pedagogically. On the other hand, there is less tedium in further worlds.

[Dan Velleman]

Thanks for this feedback! It will be very helpful as I continue to develop the game.