# Can Category Theory help us prove P != NP?

Scott Aaronson, in this funny April Fools’ Day post, introduces a fictionalized $$P \neq NP$$ Proof and, among other things, he says that the proof make use of

Higher topos theory to solve the biggest problem there was.

More and more often I hear about Category Theory (of which the former Higher Topos Theory is part) . Some say it is one of the branches of pure mathematics that is undergoing the most dramatic developments in recent years (some say it will replace set theory as the foundation of mathematics), while others are still a bit skeptical.

I am not aware of an extensive use in Computer Science, but (it seems that) it is becoming more and more present (functional programming, type theory, data structures, etc.). Furthermore, I do not believe that Scott Aaronson mentioned it at random as a tool used for a possible proof of $$P \neq NP$$: the bird eye view it provides on mathematical and logical entities could be extremely important and help us to identify some common properties that we have never been able to see because we lacked the right tools.

My question is the following: have there been researchers who have achieved important results in the field of computational complexity using the tools of category theory? How do theoretical computer scientists see this theory?

• arxiv.org/abs/1610.07737 - check this out. Introduces a categorical definition of complexity. Oct 22 '19 at 2:14
• Related: cstheory.stackexchange.com/q/944/225. Short answer: no interesting theorems in complexity theory (so far) have been proven using category-theoretic tools, as far as I know. But other topics in theory have some such theorems. Oct 22 '19 at 20:40
• It is an extensively used mathematical tool in much of programming language theory and logic (in CS). Conferences like POPL, LICS and ICFP now even have sessions dedicated to category theory.
– xrq
Oct 29 '19 at 16:42