CIRCLE WITH A DOT

@johncarlosbaez uncomfortable in many ways, yes.

@johncarlosbaez your suggestion made me think of this Far Side cartoon:
https://static1.cbrimages.com/wordpress/wp-content/uploads/2023/05/the-far-side-didnt-wash-hands.jpg

@RobJLow @johncarlosbaez Well, I heard Kevin talk about problems in the Langlands program where Jim Arthur claimed big results in a number of really meaty "forthcoming" papers and people took his word, and then it turned out there were big problems. In that kind of mathematics, the problem wasn't that it wasn't formalised, but that people are perhaps getting a bit too confident.....

@johncarlosbaez I take your point on Kevin's comment ( @xenaproject if he logs in and sees this), but a) Kevin likes making hyperbolic public statements to stir the pot b) never forget the journalist and then their editors in the process and c) what Kevin in currently doing is actually stopping to re-think how best to prove FLT, in a way that's novel and more cleanly abstracted and packaged. Perhaps this type of novel re-thinking is not happening every day in number theory, and so it feels really fun. Obviously, category theorists abstract structures and proofs all the time, so this process feels like an absolute no-brainer to us. (Nota Bene: I can also make hyperbolic statements to stir the pot).

Actually looking at the mathematics he is doing currently is really interesting, because it's making it much clearer and leaner (pun not intended), or at least exposing where the really hard core theorems are. Ideally those can subsequently get the same treatment, and people don't just cite a 150-page paper from the 70s or 80s that makes enormous effort to prove a very elementary statement as a black box, but think through if it can be improved.