OpenAI's 372 math proofs and why mathematicians are upset
- YT :: https://www.youtube.com/watch?v=WXh4LF3zJ1Q
- Original title :: The Mathematics are Mad
ThePrimeagen covers OpenAI's release on October 6th of solutions to 372 open math problems in a single day, and the negative reaction from mathematicians. In September Terence Tao published a letter, signed by many Fields medalists, saying that AI companies' goals and the mathematical community's goals are misaligned. Two concerns stand out. Mass-dropped proofs produce no follow-up activity, new collaborators or textbook digestion, which is how the field normally trains the next generation. Many results are also brute-force computational results, sometimes as huge Lean formalizations, that give no insight. He uses the integer multiplication bound and the bin packing proof as examples, notes that a Fibonacci torus view gave a more elegant picture of the packing result, and draws a parallel with software engineering and the problem of juniors.
Why mathematicians are upset
- OpenAI published 372 solved open problems at once, with Lean formalizations for roughly a hundred of them. Some of the problems would earn a Fields medal if solved. The list itself reportedly has numbering mistakes, and some answers may turn out to be wrong.
- Tao's letter of September 11th: LLM math ability has improved to the point of solving major open problems, but using math problems as an AI benchmark harms the science and the community.
- First concern: a normal breakthrough triggers talks, workshops, collaborations and follow-up problems. The proof is digested, streamlined and ends up in textbooks. A bulk dump skips all of this, so it generates no excitement and no new understanding.
- Second concern: proofs can be millions of lines of Lean, which nobody can really read. Lean is a language machines can use for proofs, and LLMs are good at producing large amounts of code, so it suits OpenAI.
- The same question applies to software: how to raise newcomers in a field where AI does the work. If everything is solved instantly, what is the purpose of learning it?
Math humans cannot do
- The bin packing result (fitting unit squares in the smallest area) has no visible pattern, only a tight arrangement found by heavy computation. This suggests part of mathematics is computation-bound and beyond human reach.
- Integer multiplication: the accepted n log n bound was beaten by a tiny exponent below 1 (a long string of nines). Doug Colkitt then reviewed the paper and in the following hours repeatedly improved the exponent saving, by factors such as 2^75, 570 million and 500,000, down to about five nines.
- The results are asymptotic and impractical, but the improvements fit the "four-minute mile" pattern: once Roger Bannister broke it in 1954, others followed quickly. The running time may head toward something like n times the square root of log n.
- The fear is that the AI proofs are brute-force and do not reach the real heart of the problem, such as an elegant bound.
Perspective
- Some problems become simple after a change of viewpoint. The Archimedean spiral is hard in Cartesian coordinates but as simple as a line in polar coordinates. Fourier transforms are another example.
- A paper by David Budden shows the planar bin packing optimum wrapped onto a torus gives the same number, and on a Fibonacci torus the structure is uniform and repetitive. So OpenAI's answer was valid, but a more beautiful solution existed under a different perspective.
- A physics joke is used for contrast: nature has fundamental constants that look arbitrary, but in the right units the speed of light is one.
Parallel with software
- Since AI became common, work on new libraries, new abstractions and better ways to view hard problems has declined, and people no longer review code.
- Software is a practical art delivering value to customers, so AI use differs from math, where the purpose is new perspectives and the optimal, elegant solution.
- r/math reportedly bans or restricts AI posts, so the 372-problem release is barely discussed there.
Takeaway
- Tao's worry about the next generation applies to programmers too: discoveries should excite and prepare newcomers to go further.
- Hand coders still build interesting things. He urges beginners to learn concepts deeply even if they type less code than before.