I hesitated a lot before writing this answer, because I feel that the current question ("*Is there any hard logic conjecture that has been proven by using categories?*") hinges on how one defines hard logic. Ideally, the question would have defined the term, or at least delineated it via some examples/non-examples of what count as "hard logic" conjectures.

In the end, I chose to bring my own definition, which may not sit well with everyone. But that's okay: everyone is welcome to share their definitions in their own responses.

In my interpretation, hard logic primarily concerns foundational theories, i.e. theories which can serve as a foundation for mathematics, but not questions about tame theories, the realm of classical model theory. E.g. looking at whether certain formal reasoning systems (like second-order propositional sequent calculi, forms of linear logic, dependent type theory, etc.) or foundational-strength axiomatic theories (e.g. HA, PA, CZF, IZF, various extensions, etc.) have key algorithmic and metatheoretical properties (ranging from consistency, not proving certain bad principles, existence properties, canonicity, projective existence, parametricity, etc.) would be considered hard logic; definitely outside the scope would be things like tame first-order theories (like ACF0, DCF0, the theory of the Farey graph, etc.) and tame properties (like quantifier elimination, stability, distality, o-minimality, etc.).

Resolving questions of interest in mathematics tends to require a combination of ad-hoc insights with general theory. A very simple example: one can prove consistency of PA in ZFC by producing a good old Tarskian model (reusable general theory), but actually producing this model requires constructing $(\mathbb{N},+,\cdot)$ and checking that it satisfies PA (a problem-specific insight).

Mathematics has managed to isolate some general, reusable theory about foundational systems, under broad umbrellas such as set theory and categorical logic. These are not entirely independent umbrellas, of course, e.g. the correspondence between forcing and categories of sheaves is widely known.

I wish to argue that for foundational-type questions, the general results of categorical logic are in fact fantastic reusable tools (even though, as always, ad-hoc insights and ideas are also required to solve difficult problems). And in response to your specific inquiry, categorical logic has indeed featured in solutions to important conjectures. Let me mention one recent example.

Normalization for cubical type theory is as "hard" as a logic question can get: it is literally an algorithmic question about a formal system of reasoning that can serve as a foundation for mathematics. First conjectured in 2016 and established by Sterling and Angiuli in 2021, the proof of normalization for cubical type theory relies essentially on *Artin gluing*, a major technique of categorical logic, done in the setting of locally Cartesian closed categories.

There are many more examples of course, hopefully to be mentioned in other answers by other people.

Now, when questioning the impact of categorical logic, it's not sufficient to be unimpressed by the standard results of the subject. One is free to argue that, even despite the contributions mentioned above, the general results of categorical logic are still somehow *too shallow* to count. Mayhap so. But it's crucial to confront the reality that the contributions are nonetheless *unparalleled*: bringing in a few key results from categorical logic does seem to help in many situations, and in those specific situations no other general body of results seems to help more, or even comparably.

Admittedly, not all logicians will find the sorts of questions mentioned above to be in alignment with their research interests (for example, if your main focus is stable theories, then you'll probably have better, more powerful alternatives to any tools that categorical logic might offer for the questions you care about). But a lot of logicians are interested specifically about questions of this type, and further interest is bolstered by continuous developments in logic-adjacent areas of computer science.

Finally, it's important to recognize not only the conjectures solved using tools from categorical logic, but also the applications that preempt potential conjectures entirely, i.e. the proactive use of categorical tools in recent research. For example, the system of this recent preprint would have been interesting enough by itself to become the subject of conjectures; fortunately, tools coming primarily from categorical logic allowed the authors to construct a model of the system and prove the theorems of interest about the theory right as it was introduced. This happens with much higher frequency in low-stakes environments: numerous "is X derivable in a weak foundational theory T" type questions have been rendered unnecessary in my own work and teaching when I could construct topos models to refute them outright. A lot of us have practical need for e.g. constructive semantics at least occasionally, and it would be a lot less pleasant if we don't know the basic result that topos models do exist, or that categories with enough structure have an internal logic. Likewise, we don't even need particularly deep results in categorical logic (like subtle existence theorems) to construct a model of, say, Synthetic Differential Geometry: nonetheless, I doubt they know whether it's consistent in the parallel universe in which categorical logic never came to exist.