Solution (source code)

= Solution

A <binary block code> is a subset $C\subseteq\{0,1\}^n$; its length is the common word length $n$, its size is $m=|C|$, and its <minimum distance> is the least <Hamming distance> between distinct words. There are $V(n,r)=\sum_{j=0}^r\binom nj$ words in a radius-$r$ <Hamming ball>, since one chooses the positions to change.

Put $t=\lfloor(d-1)/2\rfloor$. Two radius-$t$ <Hamming balls> about different codewords cannot meet: otherwise the <triangle inequality> would make their centres at distance at most $2t<d$. Comparing their combined size with $2^n$ gives the <Hamming bound>
$$
A(n,d)V(n,t)\le2^n.
$$
For the other direction, start with one word and repeatedly add any word at distance at least $d$ from every word already selected. Finiteness ensures that this process stops. At that point the radius-$(d-1)$ <Hamming balls> cover the entire cube; an uncovered word could otherwise be added. These balls may overlap, but their total size is at least $2^n$. This gives the <Gilbert–Varshamov bound>
$$
\boxed{\frac{2^n}{V(n,d-1)}\le A(n,d)\le\frac{2^n}{V(n,\lfloor(d-1)/2\rfloor)}.}
$$