I think that to a large extent this is an open problem, and I think that one reason it's still open is that not enough people are working on it. I would love to see some change here but right now I think the answer is "the community doesn't actually know".
It seems that there is evidence that certain parts of mathematics are more suited to certain axiomatic frameworks. I've heard Paulson also express this view. For example, as you note, Isabelle/HOL, which uses simple type theory, is currently the leader in late 19th and early 20th century analysis. If you want to do computations of homotopy groups of synthetic types then perhaps you want a homotopy type theory based prover. And so on and so on.
For me as an algebraic number theorist this is a problematic state of affairs, because number theory is like a parasite. Number theory has existed for 2500 years and when other areas come along it tries to incorporate them and figure out how to use them to make progress in number theory (we use analysis, algebra, combinatorics, geometry and topology, and even model theory, and everything is done using classical logic). Hence if you want to do modern number theory in one theorem prover, you have to be able to do essentially all of pure mathematics, in classical logic, in that one prover. Even something old hat like the proof of Fermat's Last Theorem uses a lot of analysis and geometry to prove a result in number theory. As has already been noted, one of the reasons that I have been strongly advocating for monolithic classical libraries like Lean's mathlib is precisely because I see it as the only viable solution for attacking research level number theory. The fact that mathlib has been used by Commelin et al to prove a theorem of Clausen and Scholze is evidence that this strategy works.
OK now let me get technical.
Historically, it seems to me that mathematicians tend over time to demand more from their foundations. Simple type theory is absolutely fine for doing classical analysis up to and including early 20th century results; work of Eberl formalising most of a text on classical analytic number theory is strong evidence for this. In Lean we are behind in analysis because we made some big decisions about doing everything in an extremely general way; for example it took a long time to prove the single-variable fundamental theorem of calculus because we insisted on setting up a huge framework of multivariable analysis and integrals taking values in Banach spaces first; had we just ploughed through an undergraduate text in real analysis we could have got there much more quickly, but that is not the mathlib style. I do suspect that in 5 years' time we will be way ahead of Isabelle/HOL in terms of classical analysis and analytic number theory, however I don't think that this has anything to do with axioms, I think that it has everything to do with momentum, and the communities involved; i.e., it will be true for sociological reasons, rather than reasons to do with axioms.
With the advent of abstract algebra in the 20th century, leading onto homological methods and then abstractions such as schemes, the concept of the dependent type came to the fore (a sheaf on a scheme is an example of a dependent type; the point is that this concept is structurally logically more complex than, for example, the Riemann zeta function). I challenged the HOL people to formalise the definition of a scheme, and Paulson et al rose to the challenge and formalised schemes in Isabelle/HOL. However they could not use the Isabelle/HOL ring theory library and had to rewrite the theory of rings from the ground up in a different way, because of limitations of the HOL logic. This did not happen in Lean; we just used Lean's rings to make Lean's schemes. Is the Lean theory of schemes usable? Yes -- people like mathematics undergraduate Andrew Yang and my PhD student Jujian Zhang and several others are slowly working through the basic MSc-level material in the theory; Yang for example defined the fibre product of two schemes recently, and Zhang defined projective schemes. Based on this I would now certainly conjecture that we can do anything in the Stacks project in Lean. But is all this possible to do in Isabelle/HOL? Well, (a) nobody knows and (b) as far as I know, nobody is trying to find out. This is the problem we face; the community is too small. Furthermore if a classical mathematician is interested in schemes and wants to try using a theorem prover, Lean would be a very natural choice for them, again simply because there is both momentum, and evidence that it's working. But does this prove that a workable theory of schemes cannot be defined in HOL or in a univalent theory? It most certainly does not. It just means nobody is trying.
Finite group theory is another interesting example. In Coq they have a full proof of the odd order theorem. I've heard many times from the computer science community the idea that it would be an interesting challenge to formalise the full proof of the classification of finite simple groups, with the justification being that it's a gigantic proof so it would be another benchmark, and that some mathematicians are uneasy about the proof because of its nature. On the other hand I've also heard mathematicians express the idea that this would be an absolutely terrible project to embark upon because who cares about tens of thousands of lemmas in finite group theory, when group theory was fashionable in the 70s and 80s but things have very much moved on since then; we have seen how much noise the Clausen-Scholze work has generated in the math community and the reason for this is that it was targetting mathematics which research mathematicians in 2022 care about, as opposed to mathematics which is now in some sense less mainstream. Again we see that there are sociological issues at stake. Would it be possible to formalise a proof of the classification of finite simple groups in Coq? Probably! Would it be possible to do it in essentially any system? Probably! Will anyone do it? Who knows; I am personally doubtful right now. It would cost so much in person-hours to type in the books into a theorem prover. Ask me again when Google have figured out how to make a machine which turns regular textbooks into formalised mathematics.
A final subtlety here is that sometimes statements which mathematicians write down have different interpretations in formal systems. For example the statement that $\pi_1(S^1)=\mathbb{Z}$ is a statement which people in univalent systems say they can prove in a few lines; however the $S^1$ they're talking about is a synthetic combinatorial $S^1$, and their $\pi_1$ is a combinatorial $\pi_1$. Of course one can prove on paper that the synthetic $\pi_1(S^1)$ is isomorphic to the topological $\pi_1$ of the topological $S^1$, but the point is that the true claim that univalent systems are good at computing fundamental groups of spheres cannot be generalised to the statement that they're good at computing fundamental groups of topological spaces, because there are plenty of topological spaces like Grassmannians which nobody knows how to define synthetically, so the methods fail.
I think that real manifolds are another very interesting test case. We have them in Lean, due to work of Gouezel and others, but this was hard won. We still (at the time of writing) are not able to do basic linear algebra with vector bundles on these manifolds, as far as I know (for example taking the tensor product of two vector bundles). Is this because of foundational issues, or is it just that we're not trying hard enough? We'll find out soon enough, I'm sure. Are other foundations better equipped to solve the problem of doing things like exterior powers of vector bundles on real manifolds? WE DON'T KNOW. Which is the best system for defining de Rham cohomology of a real manifold? WE DON'T KNOW. And we don't know because people are not working on this problem. It would not surprise me at all if somewhere in the proof of Fermat's Last Theorem we need the fact that the analytically defined de Rham cohomology of a smooth projective complex variety agrees with algebraic de Rham cohomology; this sort of stuff is crucial when trying to understand the etale cohomology of modular curves and more generally Shimura varieties in terms of automorphic forms. But nobody is thinking about this question in any prover other than Lean, and in Lean progress is slow.
Let me end then with a question which I think is terrifically important and which I would love to see progress on. Given that to do number theory you need to be able to do all of pure mathematics, is it possible to create a monolithic mathematics library in every standard theorem prover which covers all of, say, the undergraduate degree in the University of Cambridge? Note that when I went there in the late 80s we certainly covered de Rham cohomology and tensor products of vector bundles on manifolds (I make this comment to stop the usual crowd of computer scientists saying "oh surely we have an undergraduate mathematical degree by now" -- we absolutely do not and there will be a lot of work to do before we get there, at least if we're aiming for Cambridge standards). I think that if people start working on this question (which we are working hard on in Lean with mathlib and I would love to see some rivals to mathlib springing up powered by other provers with other logics -- remember that mathlib is only just over 4 years old) then, and only then, will we be able to start giving coherent answers to your questions. In particular, it's only once we actually start trying to do everything in all systems that we will begin to understand whether there are parts of mathematics which just are intrisically really hard to formalise in a usable way within certain logical frameworks.
My guess: post-1960s alegebraic geometry cannot be done in a usable way in a HOL system (of course it can be done, it's just that it might not be practical and usable). And I have absolutely no idea what can be done in a univalent system because the moment you start using a univalent system you seem to fall into some kind of univalent hole and only ever work on problems specific to univalence; this is perhaps why Voevodsky, who won a Fields Medal for proving theorems about schemes, never defined a scheme in a theorem prover, whereas in Lean a team consisting mostly of undergraduates knocked off a prototype in a few weeks (using classical reasoning; I think that this was a problem for Voevodsky). I don't see any reason why there can't be a Coq version of mathlib; again the reason it's not there is I suspect sociological rather than anything else. The point about making the library monolithic is that then you are not allowed to have more than one version of rings (or more than one version of the natural numbers; the last time I checked there were four or five variants available to Coq users) -- in a monolithic library you need a consistent collection of definitions all of which play well with each other. Once we are seeing progress like this, we'll be able to understand this question better.
