Google DeepMind researchers reported that their AlphaProof Nexus system solved 9 Erdős problems, with human mathematicians checking many of its proofs. The peer-reviewed edition of their study became public two days after OpenAI posted 722 mathematical manuscripts produced by an unreleased AI model. The study was reported October 8 in Science.

The system used multiple agents powered by Google’s Gemini language model to work on 353 open Erdős problems. For difficult steps, the agents could call AlphaProof, a model trained for mathematics. They also used Lean, software that checks whether a proof’s steps follow from its formalized statements. Agents shared promising attempts and discarded those that were not progressing.

Researchers also tested a simpler configuration on the 9 problems solved by the full system. Independent Gemini agents used Lean’s feedback but neither shared attempts nor consulted AlphaProof; they solved all 9. The simpler configuration used fewer computing resources on easy problems and more on the two toughest ones. Researchers did not determine whether it could solve any problems the full system missed. Co-author Swarat Chaudhuri said the result surprised him and suggested capable language models can tackle research mathematics with relatively simple checking tools.

Lean checks only the statement encoded for it, and a mathematical statement can be translated incorrectly into or out of Lean. An October 6 preprint identified mismatches between parts of OpenAI’s written Navier–Stokes proof and its Lean counterpart. Its authors said those mismatches do not show the written proof is wrong, but a valid Lean proof does not automatically validate an AI-generated paper. Chaudhuri said human mathematicians must think through the problem and set goals for the system; checked steps can also help them identify gaps when a proof is unfinished.

Thomas Bloom, a University of Manchester mathematician who runs a site tracking more than 1,000 problems posed or collected by Paul Erdős, said visitors increasingly competed to close problems with AI proofs they often did not understand. After speaking with the reporter, Bloom stopped marking problems open or solved and closed comments, before learning of OpenAI’s results. He said AlphaProof Nexus’s results were not at the highest level of importance, while Google DeepMind was taking a more measured approach. OpenAI says it worked with an independent advisory group on sharing practices; the group said its advice was not to test unreleased AI models on advanced mathematics, which OpenAI did.

Northwestern University mathematician Bryna Kra said OpenAI had improved its citations of past literature, but researchers widely worry that AI models accessed unpublished work, making people wary of sharing ideas. Plasma AI CTO Andrew Turner said AI is making mathematics more accessible and could help answer previously unfathomable questions. A few days after Bloom changed his site, Plasma AI announced another site to track Erdős problems that welcomes AI results. Bloom urged people to stay curious and treat AI as assistance while continuing to work through mathematical problems themselves.

Google DeepMind researchers reported that their AlphaProof Nexus system solved 9 Erdős problems, with human mathematicians checking many of its proofs. The peer-reviewed edition of their study became public two days after OpenAI posted 722 mathematical manuscripts produced by an unreleased AI model. The study was reported October 8 in Science.

The system used multiple agents powered by Google’s Gemini language model to work on 353 open Erdős problems. For difficult steps, the agents could call AlphaProof, a model trained for mathematics. They also used Lean, software that checks whether a proof’s steps follow from its formalized statements. Agents shared promising attempts and discarded those that were not progressing.

Researchers also tested a simpler configuration on the 9 problems solved by the full system. Independent Gemini agents used Lean’s feedback but neither shared attempts nor consulted AlphaProof; they solved all 9. The simpler configuration used fewer computing resources on easy problems and more on the two toughest ones. Researchers did not determine whether it could solve any problems the full system missed. Co-author Swarat Chaudhuri said the result surprised him and suggested capable language models can tackle research mathematics with relatively simple checking tools.

Lean checks only the statement encoded for it, and a mathematical statement can be translated incorrectly into or out of Lean. An October 6 preprint identified mismatches between parts of OpenAI’s written Navier–Stokes proof and its Lean counterpart. Its authors said those mismatches do not show the written proof is wrong, but a valid Lean proof does not automatically validate an AI-generated paper. Chaudhuri said human mathematicians must think through the problem and set goals for the system; checked steps can also help them identify gaps when a proof is unfinished.

Thomas Bloom, a University of Manchester mathematician who runs a site tracking more than 1,000 problems posed or collected by Paul Erdős, said visitors increasingly competed to close problems with AI proofs they often did not understand. After speaking with the reporter, Bloom stopped marking problems open or solved and closed comments, before learning of OpenAI’s results. He said AlphaProof Nexus’s results were not at the highest level of importance, while Google DeepMind was taking a more measured approach. OpenAI says it worked with an independent advisory group on sharing practices; the group said its advice was not to test unreleased AI models on advanced mathematics, which OpenAI did.

Northwestern University mathematician Bryna Kra said OpenAI had improved its citations of past literature, but researchers widely worry that AI models accessed unpublished work, making people wary of sharing ideas. Plasma AI CTO Andrew Turner said AI is making mathematics more accessible and could help answer previously unfathomable questions. A few days after Bloom changed his site, Plasma AI announced another site to track Erdős problems that welcomes AI results. Bloom urged people to stay curious and treat AI as assistance while continuing to work through mathematical problems themselves.