AI and Maths

 As an old mathematician I have been trying to follow the use of AI in maths and trying to understand what is going on. There are two aspects which are confusing me. The first is how a system like an LLM can write proofs given that it is a stochastic system that tries to work out what the next 'token' will be.  The second issue relates to how it would know that it gas a proof? There a re formal languages which have been developed, like LEAN, which can formally check that a proof is valid, at least as I understand it.  There has been a claim from Anthropic;  https://www.anthropic.com/research/formalizing-fermats-last-theorem. This turned the proof into LEAN and then used that to check. Kevin Buzzard at Imperial College has been working on this for sometime; https://profiles.imperial.ac.uk/k.buzzard. Somehow this I can understand so that AI can take a proof and turn it into code in LEAN which can then be read makes sense. 

I have tried to read the statement that Open AI published; https://openai.com/index/navier-stokes-solution/. To those who might read this who do not know me I should make clear that I am an algebraist who has worked mainly in Group Theory and have no expertise in partial differential equations of which Navier-Stokes is an example. As a consequence what I was trying to understand how AI tries to put together a proof. Progress does seem to have been quite dramatic, a recent article by Marcus du Sautoy; https://www.ft.com/content/05a7292e-4931-4631-8f77-164fb727c203, expresses this quite well.

"Please use the sharing tools found via the share button at the top or side of articles. Copying articles to share with others is a breach of FT.com T&Cs and Copyright Policy. Email licensing@ft.com to buy additional rights. Subscribers may share up to 10 or 20 articles per month using the gift article service. More information can be found on the Help FAQ on gift articles.
https://www.ft.com/content/05a7292e-4931-4631-8f77-164fb727c203

Three months ago I tried using OpenAI’s ChatGPT to assist me in my mathematical research to discover non-polynomial behaviour in the zeta functions of free nilpotent groups. It was useless. All it did was regurgitate statements in papers that I’d already published. Two weeks ago I decided to try again. The result was phenomenal. I suddenly had an insightful collaborator that knew how to code and do experiments in the structures I was investigating. It made mistakes but corrected them often on reflection. It responded to my new ideas and suggested its own. It reached a level of understanding of the issues involved that frankly would have taken a new student embarking on their PhD months to grasp. Using ChatGPT, I have now discovered very plausible evidence of the behaviour I conjectured. Because of this experiment, I was not altogether surprised by OpenAI’s recent announcement of its AI model’s successful progress on the Navier-Stokes equation — one of the seven unsolved maths problems known as the Millennium Prize Problems. "

It is not clear which version of ChatGPT he was using, possibly one that is paid for but is still not clear how the models are creating proofs by a process of working out what might come next.  

As a human mathematician my memory is quite limited but when I tackle a problem it si important to know what is already known, obviously a machine can input all the relevant data rapidly and then store it. This can be done much more efficiently and almost certainly more completely than humans.  Having gone through and hopefully understood this material you then try to see how to use it to solve the problem at hand.  Many attempts will fail but as  a human you know that and you know when you have used an argument incorrectly. This is where I get left behind, what does the AI do when it has collected all the data? I think it would be helpful to have some idea how this works, my limited knowledge come up with a few ideas but they are probably rubbish

One other concern is that as humans we come up with questions and they often feed to development of a subject.  If AI is capable of AGI then can we get it to come up with new ideas and questions. Here is a possible test: Create and AI with now knowledge after 1900, it would have to be isolated from the internet. It would have to have input data in a specified way. As the question I want to pose is about physics so perhaps it would only need to have a database of all published physics up to 1900. Would it be able to come up with relativity?