Hacker News Reader

Comment by graphlinalg | Hacker News Reader

It's interesting to suddenly get all these hits.. I haven't touched the blog in a long time.

I'm sorry that you didn't find it well-written -- it wasn't written with you in mind. Originally I wanted to write about my research in a way that was understandable to a lay person, but I quickly abandoned that and went for the mythical "second year undergrad" level.

You have pretty strong thoughts about what is "useful mathematical work". Are you the high priest and decider of the usefulness of mathematics? To be honest, it almost sounds like some category theorist was super mean to you...

One more thing. Arguments like "niche of a niche" are sociological - just because something is niche doesn't mean it's not important (or, god forbid, fun!). Maths is one of the most conservative fields in this sense; what is and is not considered "standard" is extremely political.

View on HN

I'm enjoying it so far. Thanks for taking the time to do this!

"Are you the high priest and decider of the usefulness of mathematics? To be honest, it almost sounds like some category theorist was super mean to you..."

Interesting and totally not ad hominem response... I believe Kevin Buzzard (an actual mathematician) had a few words about this last year: https://youtu.be/Dp-mQ3HxgDE?t=1039

Note that Kevin Buzzard is talking in the context of convincing "mainstream" mathematicians to use a proof assistant. He specifically clarifies somewhere (not sure where in this video, but I've seen other videos where he clarifies it) that when he talks about "proper mathematics" he is doing so in kind of a tongue-in-cheek, British way and does not mean to suggest that other kinds of mathematics are not proper (don't remember the exact wording).

In the context of that video, his comments about category theorists and type theorists make a lot of sense: type theory people and (perhaps to a more limited extent) category theory people tend to be more easily sold on using a proof assistant since the kind of mathematics they do translate more easily into current proof assistants than, say, analysis or topology.

I definitely do not think that Kevin Buzzard is suggesting that type theorists and category theorists are not doing interesting and/or useful work (after all, the proof assistant he is advocating for is based on type theory). At best, he is making a sociological observation that there is a gap between the type theory/category theory community and "mainstream" mathematicians making the widespread adoption of proof assistants in mathematics more difficult.

Given the tone of the poster who this reply was for, it seems entirely warranted.

feanaro: fine, if you think so.

I find it interesting that actual mathematicians working in Category Theory, such as Tom Leinster (who wrote a lovely little introductory text on Category Theory [not covering monads though] and made it freely available on arXiv: https://arxiv.org/abs/1612.09375) are able to engage in polite discussion about the contentious viewpoints on the use of CT without resorting to personal attacks (see 2-3 minutes from his talk from a few years back: https://youtu.be/UoutGluNVlI?t=410) ... which stands in sharp contrast to some of the evangelists, whose attitude in response to criticism often reeks of arrogance and puts people off taking CT seriously, which I think is a great shame.

Reply on news.ycombinator.com