Show that there exists no binary linear $[12,5,5]$ code.
Motivation
By the parity-bit extension, the existence of a binary linear $[12,5,5]$ code is equivalent to the existence of a binary linear $[13,5,6]$ code. I started thinking about these parameters when misreading the parameters in this question. By the codetables.de database, the code does not exist. I would expect that it should be possible to exclude such small parameters by some easy standard bound or argument. However, so far I didn't manage to do that.
I'll post my solution below, but I really hope for more insight and a simpler solution.
Assume there exists a binary linear $[12,5,5]$ code. The extension by a parity check bit gives a binary linear even (i.e. all weights are divisible by $2$) $[13,5,6]$ code $C$.
The residual of $C$ in a codeword of weight $10$ yields a $[3,4]$-code which clearly does not exist (the dimension should be at most the length). Hence there is no codeword of weight $10$. So in the weight enumerator $(a_0,\ldots,a_{13})$ of $C$, all values are zero except possibly $a_0 = 1$, $a_6$, $a_8$ and $a_{12}$. Let $(b_0,\ldots,b_{13})$ be the weight enumerator of $C^\perp$. Assuming the minimum weight of $C^\perp$ is at most $3$, shortening $C$ in $3$ positions containing the support of a minimum weight word of $C^\perp$ yields a binary linear $[10,3,6]$ code, whose existence contradicts the Griesmer bound. Therefore $b_1 = b_2 = b_3 = 0$.
Plugging these values into the first three MacWilliams identities (actually, $b_3 = 0$ is not needed) gives the fractional solution $a_6 = \frac{68}{3}$, a contradiction.