4 ms·
I know category theory is popular in CS-land but over in math land it falls squarely in the "general nonsense" bucket for most working mathematicians. E.g. mos
by rsj_hn 6y ago
I know category theory is popular in CS-land but over in math land it falls squarely in the "general nonsense" bucket for most working mathematicians.
E.g. most mathematicians learn the definitions of categories and the Yoneda Lemma perhaps as a chapter in some other text -- say a text on more modern algebraic geometry -- and that's about it.
The thing to understand is that mathematicians have jobs to do like everyone else -- they are not philosophers sitting in contemplation, but eager beavers trying to answer specific questions and solve open problems. So they are interested in picking up the tools that will help them solve unsolved problems more than picking up the tools that will help repackage the research of others. And the main feature of category theory is its ability to repackage the discoveries of others, rather than necessarily driving new research.
That's not to say that occasionally category theory can't be useful, but just not that many people are going to be working in those research fields where they find anything beyond the chapter's worth of Yoneda lemma plus some of the diagram formalism to be useful, and everyone's time and attention span is limited to what will help them make discoveries in their field.
Rarely is the answer to the question of how to solve some problem in differential geometry, pdes, number theory, symplectic geometry, combinatorics etc, -- "more category theory". The same is true for formal logic. Most people learn the incompleteness theorems and maybe even some things on computability, but they do not use formal logic to advance their research agenda, even though in theory proofs can be encoded in formal systems and so in some sense, these formal systems are a unifying framework to view mathematical proofs.
On the other hand, there have been some spectacular breakthroughs with physics/string theory, so a lot of people were trying to brush up on that. But here, too, progress is quite difficult, and most people aren't going to go out of their way to invest too much time in it beyond a summer school or so.
- jkhdigital 6y agoI am personally interested in this, as a cryptography PhD student, because the state of “provable security” is an absolute dumpster fire. In my opinion this is one particular application where machine-checkable proofs need to be established as a baseline standard. Mathematics is not a jobs program—we should be building on previous work in the most efficient and effective way we can, and getting everyone to use standard techniques that easily translate to mechanizable proofs is the only way that is going to happen.
- rsj_hn 6y agoThere are very few areas where mechanizable proofs have had success in math. I think some of the classification of finite groups was done with computer assistance, and some of the cases of the four color problem as well. But basically these are hand-crafted programs. Think of someone telling you that software engineers will be replaced by software writing computers -- that was the (failed) promise of UML. This is one of those situations where the software is generally not smarter than the person writing the code, and mathematical research, at any point in time, is driven by about 2-300 of the smartest people alive in the world at any time, with another few thousand adding finishing touches and elaborations on their work, and perhaps 10,000 adding small marginal adjustments to it. The idea that mathematicians' jobs are going to be automated by software is orders of magnitude less likely than the idea that software engineers will be automated by software. Lots of grand plans, but not much in the way of productive, transferable progress.
- jkhdigital 6y agoMy comment was not to imply that software will replace people “doing math”, but that the math which is “done” will be encoded in a standard format that can be reused (and verified) more readily. Really, this is about software—if you want to do anything with a computer, it must be formalized. Some of this formalization takes place before a line of code is written, usually in the form of mathematical statements. I’d argue that this part of the process ought to be standardized just like library code is standardized, or we will be carrying a very heavy load of collective technical debt as software is asked to do more and more complex and high-assurance tasks.
- rsj_hn 6y agoI don't quite understand -- we know that, for example, correct program analysis is theoretically impossible. There is no tool to verify a general software program. Why should there be a tool to verify a general theorem? Verification is at least as complicated as writing the program you are verifying.
- 6y ago
- _dps 6y agoI share your view of what working mathematicians think like on this subject. I summarize it thus: how many interesting theorems are there in Category Theory? And the answer you get from proponents varies, but it seems to be like 1-3 with some being kind of a stretch. I would love to learn of a body of theorems like those of analysis or topology or algebra, but by comparison there seems to be very little "there" there. I would be happy to be proven incorrect on this!
- rsj_hn 6y agoYeah, there's a lot of confusion for people using concepts like morphisms as a notation in their work versus category theory as a research program in and of itself. I don't think there is any research program there. But a lot of the more abstract topics like Motives use this language of morphisms and so people consider that to be category theory as well. I've even heard of people calling all the diagram chasing techniques like spectral sequences category theory, but I have to keep pressing the notation versus ideas distinction and give that a firm "no". If we start organizing mathematical subjects by their notational or bookkeeping systems, then we will not end up with useful categories (so to speak:)).
- ukj 6y agoThe thing with “solving open problems” is whether one is solving particular instances of an abstract problem or a general case of a practical problem. The latter is what software engineers call “design patterns.