Are there MD5 collisions for inputs of different length? There are many examples of MD5 collisions (some of them can be found here Are there two known strings which have the same MD5 hash value?). But as far as I know two inputs should have the same length to have the same MD5 (or same hash in general). Is it correct? Is there any proof of that?

Or otherwise examples of inputs of different lengths with the same MD5?
So the problem with different-size MD5 collisions is that our collision-finding tools aren't yet powerful enough to find them efficiently.

First we need to understand the rough idea of how MD5 works, using the Merkle–Damgård construction where essentially you keep some state $s$ and some current input block $m$, combine them with a compression-function and use the output as new state $s$, with the last state effectively being the output.

Now what our current techniques can achieve is that given (arbitrary) states $s_1\neq s_2$, they can find a sequence of message blocks $(m_1,m_1',\ldots)$ and $(m_2,m_2',\ldots)$ that when fed into the hash function will yield the updated states to be the same $s_1'=s_2'$ (this is called a "chosen-prefix collision attack").

The problem is, that after $s_1',s_2'$ the messages need to be equal (including length) to preserve the collision or you'll have to re-unite the states again if you feed different messages again. This is a problem because MD5 appends the length of the processed message to the message just before feeding of to the final compression function call. In particular that means that when you use different-length messages your last blocks will differ and as it is the last block you can't just feed message blocks to make up for this difference again.

In theory you could try to defy this problem by either finding a collision on the compression function that involves this little control on the last few bytes, but practically it appears nobody has done this (yet).

However, if you are looking for a brute-force collision, which would entail about $2^{64}$ expected work and $2^{128}+1$ worst-case work, you can just have a 128-bit counter $\mathbb i$ and continually hash $\mathbb i$ and $\mathbb i\|\mathbb i$, looking for hashes which appear in both sets. Any such entry, which is guaranteed to exist after $\mathbb i$ cycled through its whole range will be a different-length collision.