Ghani, a category theorist at Strathclyde, was talking with Thorsten Altenkirch and Deniz Sarikaya about what LLMs are doing to mathematics. He uses Claude heavily and rates it, and the point of the story is that he knows enough to catch it. What worries him is senior colleagues repeating model output they cannot check, which he thinks closes down the space for inquiry.
…just stuff published. And, you know, do you really need all those papers? No one thinks we really need all those papers. And it's driven not even by the mathematicians. It's often driven by university bureaucrats who want to measure stuff and they just weigh the papers. That's not mathematics.
…will make the social structure change, hopefully for the better. The only thing where I really, really worry is learning, because I think there is immense value in doing the messy detail work for a while. I worry. And then later on, we get this weird, you are now allowed to skip over the details.
Yeah. I worry too. I've seen a number of problems of AI. And so apart from the political and social aspects and whatever. It used to be that if you didn't know the answer, you said, I don't know the answer. Now you go to Claude and you trot out some stuff that Claude says and you think it's true. And this is really bad. And I've seen a lot of senior people, you know, they go around, they do this kind of thing, they trot out stuff, they don't know what they're talking about. And this is really, really dangerous because it's going to mean that the space for inquiry gets closed down because people think they know the answer, but they don't know what they're talking about. That's not good. Another real problem is, so Claude, for me, I use a lot of it. I think it's fantastic. It helps me do things, but I know more than Claude. Theory Meets, Claude is like a 26-year-old precocious PhD student. Yes, works hard, does lots of things, talks crap quite often. I mean, I told Torsen recently, Claude told me that the category of containers is locally cut easy and closed. It's not. And he gave me a sketch proof. And, you know, if you don't know…
I mean, I've got this very concrete problem. I'm teaching logic. And how do you finish logic? It's called I'm using a proof assistant. A while ago, I used cock when it was still cock. And now I'm using lean. Now the problem is I set them some exercises and the exercises are formative, really, but I…
The exit is there. Then everybody is safe.
Yes. So then, but it was really good because they were stuck on something and then you walked around the lab and give them little hints and they learned something. And now they can just use an AI and AI will fill in the proof. And that's too easy.