Theorem:
A year has a leap week if and only if the corresponding Gregorian year
either starts on a Thursday or ends on a Thursday.
Proof (Rudolphe Audette):
Under ISO, a week (ISO-defined as Monday through Sunday) belongs to the
civil year to which its Thursday belongs. So any year encompassing 53
Thursdays has 53 weeks. This happens for any year (common or leap)
beginning on Thursday, thus ending on Thursday (common) or Friday (leap).
It _also_ happens for leap years beginning on _Wednesday_, thus ending on
Thursday.