There is a relatively well known math game by the name of proset that, simplified, works as follows: You and your opponent are both given seven natural numbers with no more than six binary digits, and asked to find a non-null subset of the numbers such that the binary xor of them is equal to zero. In the game, it is assumed that this is always possible, and I am looking for a proof of this.
My attempt: I begun by rephrasing the problem so that we attempt to find two distinct subsets which xor to the same, not necessarily zero, value. From these two subsets, we can then take all numbers only in one of the subsets and these numbers will then create a valid subset that xor's to zero (this step can be thought of as xor'ing the subsets). One part of my question concerns how this can be formally proven.
Once we have this simplified problem, the solution seems rather trivial by the pigeon hole principle- There exist $2^7-1$ subsets each of which take on a value in the range $\left[0, 2^6-1\right]$ and so two such subsets must have the same value.
My question is whether the simplification is valid and does not leave out any edge cases or have other mistakes, how to prove that it is valid/invalid, and whether after this simplification the proof I provided is correct.
Your proof is correct (and your 'simplification' is valid), and your proof is a rather clean combinatorial proof.
For another popular proof, note that any set of seven vectors of $\mathbb{F}_2^6$ is linearly dependent, where $\mathbb{F}_2$ is the finite field on two elements.