Absolutely agree. There's some interesting articles in a recent [AMS Bulletin](https://www.ams.org/journals/bull/2024-61-02/home.html?activ...) giving perspectives on this question: what does it do to math if there's a strong theorem prover out there, in what ways can AI help mathematicians, what is math exactly?
I find that a lot of AI+Math work is focused on the end game where you have a clear problem to solve, rather than the early exploratory work where most of the time is spent. The challenge is in making the right connections and analogies, discovering hidden useful results, asking the right questions, translating between fields.
I'm getting ready to launch [Sugaku](https://sugaku.net), where I'm trying to build tools for the above, based on processing the published math literature and training models on it. The kind of search of MR that you mentioned doing is exactly what a computer should do instead. I can create an account for you and would love some feedback.
I find that a lot of AI+Math work is focused on the end game where you have a clear problem to solve, rather than the early exploratory work where most of the time is spent. The challenge is in making the right connections and analogies, discovering hidden useful results, asking the right questions, translating between fields.
I'm getting ready to launch [Sugaku](https://sugaku.net), where I'm trying to build tools for the above, based on processing the published math literature and training models on it. The kind of search of MR that you mentioned doing is exactly what a computer should do instead. I can create an account for you and would love some feedback.