Glitches in Natural Number Game?

Stream: new members

[dk818]

the natural numbers game seems to have a glitch in the add left cancel, I shouldn't be able to do this. What is going wrong?

Screenshot 2025-12-12 154104.png

[Jakub Nowak]

It created one more goal though. You had 2 goals before applying rw[add_left_cancel 0 x y], and after, you have 3 goals.

[Kevin Buzzard]

Right -- you can click on goal 2 or goal 3 and you'll find something which isn't provable. To prove the theorem you'll have to close all the goals so there's no soundness issue here.

[dk818]

ok, I went back and redid the proofs. I realized the reason I was struggling was because I was using rw instead of apply and ended up misusing the notation to get what I needed. However, in the screenshot that I posted, I had finished the theorem since I could resolve all of the impossible cases with trivial, which shouldn't be possible? Either way, thank you guys for your help!