We have identified two forms of mathematics, (S) symbolic performed with symbols/words and (N) numerical performed by computation with numbers. The forms of AI now taking humanity with surprise are based on Large Language Models LLM exhibiting a formidable capacity to compose texts as strings of words, after training by reading many texts composed by humans over centuries.
The OpenAI proof the Clay Millennium conjecture that solutions to Navier-Stokes equations can develop singularities in finite time, takes the form of a 167 page string of words formally verified to be logically consistent as a consequence of known already proved theorems. The proof does not present the values of the singular solution in numerical form, only that such a thing must exist as a logical consequence of know theorems taking the form a string of words thus an example of (S), exactly what LLMs are designed to do
RealQM is a new form of quantum mechanics developed with Claude as coding agent and producing numerical solutions to concrete problems of quantum mechanics without other input than case specification thus without free parameters asking for observational input. This represents (N) as numerical computation, which is not a string of words but a string of purely computational tasks. It shows that Claude is very capable of producing efficient code performing the tasks specified by an algorithm for numerical solution of the Schrödinger equation of RealQM needed as starting point. This algorithm is not a proof but a list of tasks obeying logics. The list of basic tasks in numerical computation is limited; basically addition and gradient or fixed-point iteration, at least in the context of physics with equations such as Navier-Stokes.
That Claude can code is not the result of reading massive text, but comes from logic combined with knowledge of numerical algorithms. The training as LLM can then help with logic.
So it is maybe not so surprising that AI can produced lengthy proofs of mathematical theorems, may better and more expedient than real top mathematicians, as an LLM. More surprising maybe that AI can code, which ultimately does not need so much of intelligence.
There is an important difference between step-by-step formal verification of a symbolic proof of some mathematical theorem, which can overwhelming for long proofs with many steps, and assessment of the quality of a computed solution which can be done by a posteriori evaluating its residual without checking every step.
A numerical solution can be time-consuming to compute but quick to check. N vs NP.

Inga kommentarer:
Skicka en kommentar