From what I understand, the majority of these results involve vast amounts of calculation. Nobody has said wow, AI devised a whole new technique / concept to solve this problem. I would be seriously worried if it had done, but it didn’t, so I’m not. `Calculation’ includes number-crunching, algebraic manipulations, the operations of the calculus, solving PDEs by using Fourier or other series, and anything else algorithmic in nature.
Now excuse a brief technical interlude.
Let s be any statement in (the language of) a consistent theory, then the theory is
Semi-decidable, if there is an algorithm that can determine (in a finite number of steps) if s is true, but not necessarily if it is false
Decidable, if there is an algorithm that can decide in a finite number of steps if s is true or if it is false
Productive, if any algorithm that finds true statements of the theory, never finds all of them
Creative, if any algorithm that finds false statements, never finds all of them
It is not possible to enumerate all the true statements of a productive theory, nor the false statements of a creative theory, so creative and productive theories are undecidable. Which means there is no algorithm to check whether a statement (in the language of the theory) is true or not.
Some theories are decidable: Skolem arithmetic, Boolean algebras, real-closed and algebraically-close fields, Euclidean geometry and abelian groups for examples. The general theory of groups, and even finite groups, is undecidable, as are the first-order theories of integers and rational numbers with addition, multiplication, and equality. A subtlety is that one theory might be undecidable, but a sub-theory of it might be.
A theorem about `all numbers’ is first-order, but a theorem that uses subsets of numbers - as the induction axiom for natural numbers does - is second-order. Algebraic theories - e.g. the theory of rings, are usually first-order, but all the interesting theorems are second-order, e.g. theorems about ideals, quotient rings, Noetherian rings, and so on. In general, the second-order theorems about a type of algebraic structure are undecidable. Topology is second-order right from the start, and so is real analysis, since the completion axiom refers to subsets of the real numbers. Any second-order theory that contains Peano arithmetic is undecidable, and indeed productive, and that is all the interesting ones. It even includes categories with natural number objects. Try doing anything interesting without using the positive integers.
This means there is no general-purpose algorithm for producing proofs of the kind of theorems mathematicians want to prove, which are about the relationships between different properties of mathematical structures (`All cyclic groups are abelian’ for a simple example). There might be specific algorithms for certain collections of statements, but there is no all-purpose one. This matters because a theorem is a statement with a proof - until then it is a conjecture.
So proofs have to be found by luck, insight, experience or other non-algorithmic means, all of which are fancy ways of saying `trial and error’ or even `guessing’. If there is one thing that can trial-and-error for hours and days on end without tiring, it’s a computer. When a computer running a program that can start at the frontiers of published research, take some guesses, self-correct, and guess some more, which is what LLMs and all AI systems do, we should not be so surprised if it finds a solution now and again. (After all, though OpenAI produced 270 results, they are keeping very quiet about how many attempts they started with. Unless I missed something.)
After all, experience with chess computers has taught us that, if you play computationally, a suitably-programmed computer will eventually just outthink you. (And chess is decidable - just not in our lifetimes, or anyone else’s.) The open-source engine Stockfish is held to be able to beat even the current champion Magnus Carlson every time. This could matter less. Chess is a game between people, and championships are there to find the current best player. Saying that it means nothing because there’s a computer program than can beat them all is the same as saying that the 440-yard dash means nothing because the record is 44.5 seconds, and a Top Fuel dragster could cover the same distance from standing in under 6 seconds (if they still did the quarter-mile).
It could also matter less if AI started producing theorems - statements with proofs. Doctoral students having been achieving instant obscurity doing that ever since von Humboldt cursed us with the research PhD over two hundred years ago. Maybe much of those two hundred years of research will be seen as `PhD slop’. What matters is that the result, and the techniques used to get it, are held to have solved interesting outstanding problems, and create promising new lines of research. Those are judgements only people can make. (Enough methodology.)
This is not the first time that machines have displaced human math skills. Calculators made old-school numeracy redundant (or at least that’s what everyone thought until they saw the results in secondary-school maths). Computers were never seen as a threat, because it was obvious from the start that the computer needed algorithms to do its calculations, and the praiseworthy human ingenuity was in the creation of algorithms and indeed of hardware design.
In the same way, I suspect that AI tools will be useful for solving problems that we may suspect are actually all about a kind of brute-force trial and error. The praiseworthy ingenuity will be in training the models on the right range of data, and tailoring the black-box algorithms of the AI to the problem. On a whim, I asked about outstanding problems in category theory and got the Simpson Conjecture. You know the one: \textit{every weak $\infty$-category is equivalent to an $\infty$-category in which composition and exchange laws are strict and only the unit laws are allowed to hold weakly}. That feels like something an AI could trial-and-error. Counter-examples cannot be reasoned into existence, and require trial-and-error: AI seems to have done something like that with the Navier-Stokes problem. That counter-example (as I understand the simple explanation) uses a flow that is subject to periodic impulses, and that’s not quite the intention of the original problem, but it is an interesting starting-point.
The mathematics-is-dead-and-AI-killed-it line comes from a mis-understanding of maths, which is that it is about calculation. That’s the bit undergrads and school pupils see, page after page of calculations and a few simple proofs, most of which also involve calculations. That is not what creative maths is. What wins Fields Medals, and more often than not has solved Hilbert’s problems, is a mixture of conceptual and technical novelty, ingenuity, and heroic calculation. Fame is attached to new ideas and their applications. The `400-page proof’ is a comparatively recent phenomenon, and nobody likes them, because nobody understands them. It might prove, but it does not explain. It’s explanation that counts.
We should not be worried about the effect of AI on maths, though mathematicians may have to adjust to revering heroic calculation less. What we need to be worried about is its effect on Liberal Arts PhDs and papers. After all, most of these are about demonstrating a mastery of a given canon of (usually) ideology. And nothing churns out re-combinations of ideological dogma better and faster than AI.
No comments:
Post a Comment