OpenAI says secret AI model prompts hundreds of public mathematical problems at a time-mathematician

OpenAI released 722 math manuscripts on GitHub on Tuesday. These are generated by the company's internal models, which are not yet public. An OpenAI spokesperson said that almost all results stem from a single prompt sent to a single AI agent, although some results may require multiple attempts to achieve. [TAG

Bold Claim vs. Cautious Examination

This is a bold claim and may mark a major breakthrough in mathematics. However, not everyone is buying or welcoming it. "Until they release the model and allow others to replicate the results, I think the claim that 'a single prompt solves complex problems' should be treated as unconfirmed speculation." "We need to see the evidence," Massachusetts Institute of Technology mathematician Andrew Sutherland told Scientific American.

These papers are classified into 372 "families", each family containing a set of related research results, which can bundle main theorems, auxiliary arguments, corollaries, or alternative proofs. Therefore, the number 722 refers to the number of manuscripts, not the number of problems solved. According to OpenAI, they asked about 4000 questions to the model and retained outputs deemed important enough to warrant publication.

Computing Resources and Verification Limitations

According to OpenAI, the average calculation consumed per result is equivalent to about three hours of reasoning power for ChatGPT Pro users. This is in sharp contrast to last month's assertion of the Navier-Stokes equations, which involved 10,000 co-agents and took 88 hours.

OpenAI only published simplified reasoning summaries for 10 of the results. In addition, according to the formal catalog in the warehouse, only 162 of the 722 papers had main results verified by computer. This accounts for about 22% of the entire collection, which has been transformed into Lean, a software tool that mechanically checks every step of logic.

OpenAI itself acknowledges that not all manuscripts have Lean formal verification and that "some unformalized results may be flawed." In other words, a lot of the content they publish may have errors. Lean's quick inspection only confirms that the proof process conforms to the statement written in Lean, does not prove that the statement is consistent with the original problem, nor does it prove that the result is novel or important-which is what mathematicians currently need to judge.

Academic community reaction polarization

This is where researchers are worried. "What's happening now is that AI can output mathematical arguments without humans being able to understand, verify or take responsibility for it." The Institute for Advanced Study in Princeton, New Jersey, said in a statement,"We believe that human understanding of mathematics remains critical. In this new era, how do we move towards a new paradigm that makes human understanding of mathematics an integral part of responsible academic output?"

Professor Abhishek Saha, on the other hand, is quite excited. "This is a big day in mathematics," he wrote. But he also pointed out that most of the issues were "extraordinary progress within existing plans" or "surprising breakthroughs" rather than a complete game-changer type.

This means that most of the questions in the collection, while interesting, are not as insurmountable or transformative as the Millennium Award problems. Among the 722 problems, the only one occupying this special position is the Quasi-Riemann Hypothesis.

Lack of transparency and future outlook

The release also fell short of the standards recommended by the Princeton Institute for Advanced Study Advisory Group on September 29: including model name, prompt words, summary of the thought chain, time spent on each result, and calculation cost. OpenAI released average calculation data and 10 reasoning summaries, but did not disclose the prompt words, and said it is still working to publish the model in a responsible manner.

Daniel Litt, a mathematician at the University of Toronto, takes the opposite view and sees no reason to require companies to keep answers to these mathematical questions confidential. In contrast, Anthropic took a different path last month, with its Lean verified proof of Fermat's Last Theorem containing 13 million lines of code and all made public on GitHub. The proof is a formalization of a theorem published by Andrew Wiles in 1995, rather than claiming new results.

OpenAI said it will supplement Lean's formal content as more verifications are obtained; currently, 162 of the 722 manuscripts have completed this work.