[Amadiro]

Yeah, I'm aware that some projects that apply computer science to pure mathematics (in various forms like Kenzo/CAT, PLEX (not CPLEX, that's for applied mathematics/finance/etc), agda, coq, GAP, ...) exist, but I don't think the claim that they are very very niche with mathematicians is exaggerated.

If you go to your average mathematics department and ask a few professors there that work in logic, algtop or alggeom, I doubt you'll find any that do any programming for their research. You probably won't find that many logicians that use proof-assistants either, although those are probably the least niche category of the things listed (and they are fairly popular with the CS folks)