It is a classical theorem. For given integer $n \ge 1$, among ${n\choose{n/2}} = 2^{(1-o(1)n)}$ strings in the cube $\{0, 1\}^n$ with weights $n/2$, i.e., $n/2$ indices are 1, there are at least $2^{cn}$ of these strings such that each pair has Hamming distance at least $n/4$, where $c$ is a constant between $0$ and 1.
This is for sure a known result. I hope to be aware of its name.
I don't have a name for the theorem, but I can give a quick proof in case you don't get hold of a name: Let $S$ be a maximal set of $n/4$-separated strings in the weight $n/2$ slice. Then the union of $n/4$-Hamming balls centred at elements of $S$ covers the entire slice. But each Hamming ball has $\binom{n}{0}+\ldots+\binom{n}{n/4}\sim 2^{an}$ elements, where $a=-\frac 14\log_2(\frac14)-\frac 34\log_2(\frac 34)<1$. Hence $S$ must consist of at least $2^{(1-a)n}$ elements.
