I present some recent joint work with Dag Normann (University of Oslo) on the Reverse Mathematics of real analysis and related areas. In particular, we have established the following, working in Kohlenbach's higher-order framework.
(a) There are many equivalences between the second-order Big Five and basic third-order theorems from real analysis.
(b) Slight variations and generalisations of the theorems from item (a) cannot be proved from the Big Five and much stronger systems.
(c) The theorems from item (b) can generally be classified as equivalent to one of four `new' Big systems, namely the uncountability of the reals, the Jordan decomposition theorem, the Baire category theorem, and Tao's pigeon hole principle for the Lebesgue measure.
(d) Basic theorems about compact metric (or: second-countable) spaces and weak continuity readily yield countable choice and even full second-order arithmetic in its various incarnations.
(e) The results in item (d) readily give rise to new equivalences for the two strongest Big Five systems and $\Sigma_1^1$-AC$_0$.