I am a producer of math. But I feel two ways about AI math.

First I fear slop-math. People producing LLM “proofs” and prose with no value. I do not want to review something the author has spend lies energy on than I will spend reviewing.

Two, I am excited about formal machine-checked proofs. I love formalisation, and if the llm can prove my lemmas I will be a happy camper!

I think my optimism here is coloured by the fact that I am a theory builder, not a problem solver. I will be happy to create beautiful theory, writing (myself) wonderful articles explaining them, but letting the ugly details be formally verified by an LLM.

A problem solver kind of mathematician might feel cheated of all the fun of the llm did all the problem solving.