I've never noticed this quirk until now, and it's screwing with my mind. Why was HTML 4.01 numbered with a leading zero, rather than as 4.1?
I don't know for sure why it was done in this specific case. But generally, it's done when someone sees the possibility that there may be more than 9 dot releases. If you go from 4.1 to 4.2 to 4.3, you're rather stuck when you're at 4.9 and want to go to 4.10 because half the software out there is going to treat that as numerically equivalent to 4.1. If you go from 4.01 to 4.02, you don't have a similar problem until you've made 99 dot releases.
Intuitively, it's because 4.01 is just a teeny bit different from 4.0, not different enough to be a 4.1 release. Many version numbering schemes would often make that a 4.0.1 release. The fact that it wasn't done this way makes me think that there may have been some known cases where the version number was being interpreted as a real number instead of as a version "number" string.