Comment by lacker

I think AI for mathematics will help us solve unsolved problems. There should be a virtuous cycle during its development.

1. More formalized training data makes the math AI better

2. Better math AI helps us formalize more known mathematics

But right now math AI is not very useful. It isn't at the point where ChatGPT is for programming, where the AI is really helpful for a lot of programming tasks even if it isn't superhuman yet. So the virtuous cycle hasn't started yet. But I think we will get there.