I stumbled upon a website called metamath that claims that all theorems can be deduced directly from the ZFC axioms. Here is the exact claim:
Essentially everything that is possible to know in mathematics can be derived from a handful of axioms known as Zermelo-Fraenkel set theory, which is the culmination of many years of effort to isolate the essential nature of mathematics and is one of the most profound achievements of mankind.
Is it really possible to be able to do this?
The metamath website does contain the somewhat brash claim:
I think it is true to say that the vast majority of mathematics can at least in principle be formalised in ZF set theory, but there are certainly things that cannot be proved in ZF, e.g., the consistency of ZF. Stronger systems than ZF have been proposed and are used, e.g., set theory with Grothendieck universes as advocated in Cohn's Universal Algebra, and Mostowski-Kelley-Morse set theory, which is well-known via from the presentation in Kelley's General Topology. Both these systems are strong enough to prove the consistency of ZF.
Tools like metamath make it possible to carry out formalisations in practice and not just in principle, but they don't provide a way round the incompleteness theorems.