Well, I had a go at this encoding thing myself. The following were the results for a 111-second video:
avi, XviD: 3257 KB
mp4, x264: 2646 KB, and noticably better quality
Is that kind of size difference (maybe 1/6) and quality enough to make mp4 the standard? Bear in mind that not everybody's got VLC.
In the meantime, I have to fix up the issue my computer has with recording sound. :/