Comment by fatbird

Much progress has been made in mathematics by demonstrating that problems in one realm are logically equivalent to solved problems in another realm, allowing proofs from the other realm to support proofs in the first. The most obvious example is the solution to Fermat's Last Theorem by Andrew Wiles, which wended far afield through the Taniyama–Shimura conjecture involving elliptic curves and modularity.

So in theory, with a solid foundation for mathematics, and new work rigorously tied back to it, this sort of thing should be both easier and more efficient.