And I think that anyone who makes even the slightest substantial contribution to homotopy type theory is doing interesting, original work.

I partially respond to this here.

I think the Low-Hanging Fruit Complaint is more often a result of not knowing where there's a hot, productive research frontier than of the universe actually lacking interesting new mathematics to uncover.

There's a lot of potential for semantic differences here, and risk of talking past each other. I'll try to be explicit. I believe that:

• There are very few people who have a nontrivial probability of discovering statements about the prime numbers that are both true, that people didn't already believe to be true, and that people find fascinating.
• The same is not far from being true for all areas of math that have been mainstream for 100+ years: algebraic topology, algebraic geometry, algebraic number theory, analytic number theory, partial differential equations, Lie Groups, functional analysis, etc.
• There is a lot of rich math to be discovered outside of the areas that pure mathematicians have focused on historically, and that people might find equally fascinating. In particular, I believe this to be true within the broad domain of machine learning.
• There are few historical examples of mathematicians discovering interesting new fields of math without being motivated by applications.