Agree with the last sentence. I think in a majority of the fields, lines of investigation with higher insight-per-effort, in the current margin, are those done with choice (or with even more controversial things like the large cardinal axioms).
Edit: this comment by Terence Tao also expresses a similar perspective:
In general, it seems that infinitary methods are good for “long-range” mathematics, as by ignoring all quantitative issues one can move more rapidly to uncover qualitatively new kinds of results, whereas finitary methods are good for “short-range” mathematics, in which existing “soft” results are refined and understood much better via the process of making them increasingly sharp, precise, and quantitative. I feel therefore that these two methods are complementary, and are both important to deepening our understanding of mathematics as a whole.
Agree with the last sentence. I think in a majority of the fields, lines of investigation with higher insight-per-effort, in the current margin, are those done with choice (or with even more controversial things like the large cardinal axioms).
Edit: this comment by Terence Tao also expresses a similar perspective:
Ah I really need to write a megasequence about the large cardinal axioms! They’re awesome (I wrote a thesis on them).
Consider my vote to be placed on writing that megasequence, I know next to nothing about large cardinals and would be eager to know more about them!