I think I may be missing something. Why would you be interested in the automation of theorem production? Wouldn’t this make mathematicians obsolete? How far away do you think we are from that?

I ask as a newbie in math; math is a passion of mine. I am genuinely reconsidering going into math research as I fear just being automated away.