Comment by black_knight

I am a mathematician, and I agree with you here. I do not feel at all threatened by LLMs, because for me the joy of mathematics is in constructing the theories and beholding their beauty! I know other people are different from me here. I find having to prove theorems a rewarding part of the whole, but I am also not going to weep if an LLM can unstuck me on difficult proofs.

I am really excited if LLMs means more of mathematics will be formalised. Once we have all of mathematics formalised, I think we will start to see real great progress!