We would be interested in actual automation of theorem production, but this pipeline would automate approximately 0% of (interesting) mathematics research. It does have the potential to automate some boring parts and enable mathematicians to make better conjectures faster.
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.
