We study the logical and computational properties of basic theorems of uncountable mathematics, including the Cousin and Lindelof lemmas, published in 1895 and 1903. Historically, these lemmas were among the first formulations of open-cover compactness and the Lindelof property, respectively. These notions are of great conceptual importance: the former is commonly viewed as a way of treating uncountable sets like e.g. [0,1] as 'almost finite', while the latter allows one to treat uncountable sets like e.g. the real numbers R as 'almost countable'. This reduction of the uncountable to the finite/countable turns out to have a considerable logical and computational cost: we show that the aforementioned lemmas, and many related theorems, are extremely hard to prove, while the associated sub-covers are extremely hard to compute. Indeed, in terms of the standard scale (based on comprehension axioms), a proof of these lemmas requires at least the full extent of second-order arithmetic, a system originating from Hilbert-Bernays’ Grundlagen der Mathematik. This observation has far-reaching implications for the Grundlagen's spiritual successor, the program of Reverse Mathematics, and the associated Goedel hierarchy. We discuss similar theorems relating to the gauge integral, a generalization of the Lebesgue and improper Riemann integrals that also uniquely provides a direct formalization of Feynman's path integral.