The actual conjecture that was proved has a very elementary formulation: if you consider all n-bit words and take any set of more than half of them (i.e. at least 1+2^(n-1)), then this set will contain some word for which there are at least √n other words in the set that differ in exactly one bit position.

For example (with n=64), if you take any set of 1+2^63 (or more) 64-bit words, then for some word in this set, there will be at least 8 other words in the set that each differ from this word in only one of the 64 bit positions.

To illustrate, here's a brute-force verification in Python for the n=4 case, that tries all (16 choose 9) = 11440 subsets:

    import itertools
    n = 4
    m = 2

    def degree(word, s):
        """How many other words differ in one bit position"""
        return sum(1 for w in s if bin(word ^ w).count('1') == 1)

    words = range(2**n)  # All n-bit words
    for s in itertools.combinations(words, 1 + 2**(n-1)):
        assert any(degree(word, s) >= m for word in s)

Note that the test fails (for 48 out of the 11440 sets) with m=3 in place of m=2, so the bound is tight in this case.