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.

[Nilesh]

Are the hints or solutions for the set theory game available somewhere? I'm stuck at the theorem comp_comp.

[Mario Carneiro]

what is your work so far?

[Nilesh]

image.png

[Mario Carneiro]

you should unfold the definition of x ∈ Aᶜ

[Kevin Buzzard]

The answer to the question is that if you find the GitHub repo for the game then the solution to a level will be in the file defining the level. For this particular question I'd be tempted to ask exactly what you've proved recently before this level.

[Dan Velleman]

Since your goal is the implication x ∉ Aᶜ → x ∈ A, I think the natural next step is to assume x ∉ Aᶜ. If you introduce that assumption, you will get a new hint suggesting proof by contradiction.

[Dan Velleman]

If you follow Mario's suggestion of first unfolding the definition of complement, you can still then follow the same procedure: intro followed by by_contra.