Google DeepMind researchers say an AI system they built, AlphaProof Nexus, has solved nine of the 353 open problems it tried from a well-known list of more than 1,200 posed by the mathematician Paul Erdős and his collaborators, including two that had been open for 56 years. The work was published in the journal Science on Oct. 8, after review by outside experts. The same system proved 44 of 492 unproven claims about number sequences listed in the On-Line Encyclopedia of Integer Sequences, a large online catalog of such sequences, settled an open question in algebraic geometry and improved a known result in optimization.
The key is how the system's proofs are checked. The researchers say the AI models behind chatbots can make subtle logical errors when they write proofs in ordinary language, so those proofs need expensive checking by experts. AlphaProof Nexus instead writes formal proofs, proofs written in a special programming language, such as Lean, so that a computer can check every step. Google's Gemini AI model proposes the steps, Lean checks them after each try, and when a step fails, Lean's error message guides the next attempt. A proof counts only when Lean accepts it with no step left unproven.
OpenAI is adding computer-checked proofs to its own public collection of math results from an internal AI model. On Oct. 7, it withdrew three of the papers in that collection, after a sign error broke an argument in one of them and the two papers built on it. OpenAI says about 42% of the main results in the collection now have proofs a computer has checked.
The researchers say the full system's computing bill came to a few hundred dollars for each problem it solved. That figure leaves out the computing spent running it on all 353 problems to find the ones it could crack, and the cost of AlphaProof, an earlier proof tool built for math-olympiad problems that the system can call on. When the researchers later gave a much simpler version, one that only passes work back and forth between the AI model and Lean, just those nine problems, it solved all of them, more cheaply on most, though it cost more on the hardest ones. All the computer-checked proofs are public on GitHub, and the results first appeared online on May 21, before the journal's review.
The system did not solve the other 344 Erdős problems it tried. A computer check also proves only the problem as it was typed into Lean, not that the typed version matches the question mathematicians meant. Josep Curto of the Open University of Catalonia says that means the system still needs close oversight by experts. The researchers say experts on their team confirmed that each solved statement matched the original question, and that the system turned up some typed versions that were wrong.
Some mathematicians are also weighing what results like these mean for their field. Javier Aramayona, director of the Institute of Mathematical Sciences, a joint institute of Spain's national research council and three universities, says the main goal of math research is understanding, and warns of a growing number of results known to be true that no one fully understands. Science ran the paper alongside a commentary by Jeremy Avigad and Matthew Ballard titled "AI for research mathematics has arrived." The researchers say the system is already being used in research on combinatorics, optimization, graph theory, algebraic geometry and quantum optics.