OpenAI Posts 722 Math Papers, Most Unverified

San Francisco — OpenAI, the company behind ChatGPT, has published 722 mathematics papers produced by one of its unreleased artificial intelligence models, a single release that mathematicians say is as striking as it is hard to digest.

The papers went up this week on GitHub, a website mostly used to share computer code, rather than in a journal or on a preprint server, the online archives where researchers usually post new papers before formal review. New Scientist, the British science magazine, reported on the release on 7 October.

What OpenAI released

According to the release notes on GitHub, the collection holds 722 manuscripts grouped into 372 "families." A family is a set of related papers, such as a main result plus follow-up arguments or alternative proofs. Each family is sorted by branch of mathematics.

OpenAI says the papers were produced by "an internal OpenAI model" that it has not named or released. The company says it expanded its tests to open research problems after its models had maxed out its existing math tests. Over the course of the project, the model was given about 4,000 problems. On average, each result used about three hours of computing on ChatGPT Pro, the company's highest-tier plan, OpenAI said. It then grouped the output and kept results it judged significant enough.

The collection includes work on well-known questions, including a region where the Riemann zeta function, a central object in the study of prime numbers, has no zeros. OpenAI said that piece and a claimed proof of a special case of the Hodge Conjecture were produced outside its standard method, and that the write-up of the zeta result was edited by humans for readability.

The checking problem

In mathematics, a result counts only once it is proved, and a proof is either right or wrong. A growing way to check proofs is to translate them into Lean, a computer language in which every logical step can be checked mechanically by software.

OpenAI's release is only partly checked this way. "Not all have accompanying Lean formalizations," the company wrote, adding: "Some of the unformalized results could have issues. We will endeavor to fix any such issues quickly."

New Scientist's Jacob Aron counted that the company's Lean catalogue lists only 162 of the 722 papers as having their main results checked by computer. Counting any Lean code at all, 235 of the 372 families have some, he wrote. Even for the checked papers, he noted, no one has yet confirmed that the computer versions match what the written papers say.

What mathematicians said

One paper claims to settle Wall's D(2) problem, a question in topology, the study of shapes. Francis Johnson of University College London worked on it for many years.

"I worked on this problem for 25 years. I produced two books on it. I, personally, gave up," Johnson told New Scientist. "I'm surprised that [AI] has done it quite so quickly, but I'm not surprised that it's done it."

Kevin Buzzard of Imperial College London urged caution. He told the magazine that 30 of the papers were in his field, number theory, that only seven of those looked impressive to him, and that only one of the seven was checked in Lean. "Acceptance of these results by the community will take time," he said.

Ben Allanach of the University of Cambridge criticised the sheer size of the release and how little was done to explain it. "Is it coming into the cadre of human knowledge?" he asked.

A guideline fight

An independent body, the Advisory Group on Mathematics and Artificial Intelligence, was set up after earlier complaints about how AI companies were releasing math results. Terence Tao of the University of California, Los Angeles, had compared such releases to "dumping carcasses of raw meat onto our communal village table," New Scientist noted.

The advisory group recommends that companies name the model, release the prompts, give the cost of computing, formally check proofs where possible, and say how many problems the model tried and failed. New Scientist reported that OpenAI's release seemed to go against many of those recommendations, and that the group said its advisory role should not be read as an endorsement of the release.

"For future releases, we are committed to further improving the quality of the papers via the citations, mathematical exposition, and presentation of the results for better understanding," OpenAI spokesperson Lindsay McCallum Rémy told the magazine. "We want to give the mathematical community time and space to assess this work."

Why it matters

Last month, New Scientist reported, OpenAI solved a problem related to the Navier–Stokes equations, which describe how fluids flow. This release goes for breadth instead of depth. Buzzard said that if the new results turn out to be mostly true, the field will learn what its new normal looks like. "It has been a long time since there were humans who were experts in all of mathematics, but now we seem to have machines with this property," he said.

The release came in the same week OpenAI began rolling out new GPT-6 models to ChatGPT users.

What happens next

OpenAI says it will add Lean checks to the collection as they are finished and keep every version public, so corrections are on the record. Mathematicians will now have to check the rest by hand or wait for computer proofs.