Zulip Chat Archive

Stream: general

Topic: Set Theory Game


Dan Velleman (Nov 19 2023 at 00:43):

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

Shreyas Srinivas (Nov 19 2023 at 01:49):

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

Brandon Brown (Nov 20 2023 at 03:21):

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:ABh : A \subset B is a function xA    xBx \in A \implies x \in B, so if you applied this function to an xAx \in A you get the xBx \in B.

Notification Bot (Nov 20 2023 at 09:24):

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

Shreyas Srinivas (Nov 20 2023 at 10:08):

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 (Nov 20 2023 at 10:09):

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 (Nov 20 2023 at 14:20):

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


Last updated: Dec 20 2023 at 11:08 UTC