Proof that no DES key makes encryption identity How can we prove that no DES key makes encryption the identity function?
That is: $\;\forall K\in\{0,1\}^{56}\quad\exists M\in\{0,1\}^{64}\quad E_K(M)\ne M$
Note: anyone disproving this proposition would gain instant celebrity, which is a meta-proof that this proposition is true, but not an acceptable answer!

That proposition is false for 2DES (EE), even restricted to one key, because twice  applying encryption with the all-zero key (and the Final Swap built into the Final Permutation) yields identity.
For the same reason, the proposition would be enough to prove that DES is not closed under function composition, hence not a group [but Keith W. Campbell and Michael J. Wiener's DES is not a group in proceedings of Crypto 1992 (free access) also proves other facts. See a more extended bibliography there].
Variants of the question:

3DES (EDE) with 3 or 2 keys
3DES EEE variant
what if we remove the Final Swap of the Final Permutation (then the proposition becomes very plausible for 2DES)
$r\ge1$ rounds of DES and independent subkeys, with or without Final Swap; clearly the proposition must become false for some $r$ !


Inspired by this question.

Update: towards a solution, I have thought of

Pure brute force. Plausibly, that requires no (or very little) more than $2^{55}$ DES encryption of a constant plaintext block $M_0$, say all zero (for we can fix a key bit thanks to the DES complementation property, and a single test is enough to eliminate overwhelmingly most keys). Using the all-zero block for $M_0$, or any one invariant under final swap, has the advantage that we can answer the question for DES both with and without final swap using essentially the same amount of work.
Some work reduction, possible by enumerating the keys in a way that allows caching of the external rounds (as was done in DESCHALL, see this).
Devising a function $F:\{0,1\}^{56}\to\{0,1\}^{64}$ that slightly simplifies the evaluation of $E_K(F(K))=\!\!\!\!?\;\,F(K)$ compared to that of $E_K(M_0)=\!\!\!\!?\;\,M_0$; it seems possible to save even more work.
Expressing the problem as a Boolean satisfiability problem in Conjunctive Normal Form and throwing a state of the art solver at it. I'm pessimistic about this approach, though.

Update2: the brute force approach might have been carried as early as 1999, when:

The EFF DES cracker first solved a challenge posed more than a year ago by world-renowned cryptographer and AT&amp;T; Labs research scientist, Matt Blaze. The &quot;Blaze Challenge&quot; was designed to only be solvable by &quot;brute force&quot; cryptanalysis of DES. Mr. Blaze challenged the world to find matching pairs of plaintext and ciphertext numbers, consisting of nothing but repeated digits. Blaze himself was unaware of any such pairs until the EFF DES Cracker revealed the first known pair. It found that a hexadecimal key of 0E 32 92 32 EA 6D 0D 73 turns a plaintext of 8787878787878787 into the ciphertext 0000000000000000.

That's nearly enough to prove the question's proposition. What's missing is  that the key found is the only solution of the Blaze challenge with all-zero ciphertext, or making an exhaustive list of those that do and ruling each out from being counterexample to the proposition.
To throw something, here are simple proofs for 2-4 rounds, applicable to almost any Feistel Network. Some notation: $F_i$ denotes $i$-th Feistel round without swaps, $f_i$ denotes the Feistel function at $i$-th round, $S$ denotes the swap.
Since the initial permutation IP and the final permutation FP are inverses of each other, we can strip them away: for any bijection $P$:
$$P^{-1} \circ G \circ P = Id ~~~\Leftrightarrow~~~ G = Id.$$
We will use this trick later.
(2 rounds)

Consider a 2-round Feistel network (like in DES, with no swaps in the beginning and in the end), denote it by $G$. We want to check if it holds that
$$\forall a,b \in \mathbb{F}_{32} ~~~ G(a,b) = a,b.$$
The right output half is equal to $a \oplus f_1(b)$. This can not always equal $b$ for any $a$ (consider two distinct $a$).
(3 rounds)

Consider a 3-round Feistel network. The right half in the middle is equal to $a \oplus f_1(b)$ (from the input) and to $a \oplus f_3(b)$ (from the output). It follows that $f_1(b) = f_3(b)$ for all $b$. We can now use the trick again and remove symmetrically the first and the last round and the two middle swaps. We end up with $F_2(a,b) := (a \oplus f(b), b)$. Due to the nonlinearity of $f$ in DES, there exist no keys such that $f_2$ (and so $F_2$) is an identity (the key is only xored at the input of $f$).
(4 rounds)

Note that $(S\circ F_1)(a, b) = (b, *)$, and $(S \circ F_4^{-1})(a, b) = (b, *)$, where $*$ denotes a wildcard. So it sufficient to show that there are no 2-round FN that for all $b,x\in \mathbb{F}_{2^{32}}$ always map $(b, x)$ to $(b, y)$ for some $y \in \mathbb{F}_{2^{32}}$. For the two middle rounds we get 2 equations:
$$
b \oplus f_2(x) = y,
$$
$$
b \oplus f_3(y) = x.
$$
If in the input we change $b$ to $b\oplus \delta$ and don't change $x$, then $y$ has to change to $y \oplus \delta$ (from the first equation). From the second equation, we must have
$$b \oplus \delta \oplus f_3(y\oplus \delta) = x,$$
and so
$$f_3(y \oplus \delta) \oplus f_3(y) = \delta.$$
Since this must hold for all $y$, we obtain that $f_3$ must be a XOR with a constant, which obviously does not hold for DES rounds.