OpenAI published a roundup of ten claimed advances in pure mathematics and theoretical computer science, saying an internal model produced proofs or counterexamples for long-standing open problems and that some were then formalized in Lean. Several commenters familiar with the underlying areas treated at least some of the results as unquestionably serious. The non-sofic group construction, Connes rigidity counterexample, and the CS results around CVP and circuit complexity were repeatedly described as problems that had resisted top researchers for decades, not as toy exercises or low-value cleanups. That moved the conversation away from "is this fake" and toward "what exactly did OpenAI do, and how should this kind of work be published and credited?"
The strongest through-line was that OpenAI disclosed too little about the experimental setup for anyone to interpret the headline claims cleanly. People wanted the denominator, not just the wins: how many problems were tried, how many failed, how much iteration and expert steering were needed, and whether the quoted sub-$2,000 cost covered only successful inference runs rather than the total search process. The point was not that the proofs stop being valid if the company cherry-picked targets. It was that without the full attempt distribution you cannot tell whether the story is "cheap autonomous theorem proving" or "expensive expert-guided search that occasionally lands." That distinction matters if you are trying to understand capability contours rather than applaud a result.
A second theme was that math may need new publication norms once AI systems are major contributors. Some argued that if the formal proof checks, the origin story is secondary. Others pushed back that mathematics is not only about correctness. It is also about understanding methods, extending them, and knowing whether a result came from a reusable idea or from opaque search. That led to calls for reproducible disclosure more like experimental science: model version, prompts,
inference settings, and full proof artifacts. The release of a GitHub repo with Lean proofs was seen as a step forward, but not enough without the prompting and search history.
The mood was also shaped by a broad recognition that the economic and career consequences are now harder to wave away. A lot of comments were not disputing the raw capability anymore. They were reacting to what happens when systems can produce work that looks career-defining in elite technical fields. Some saw this as a golden age for mathematics, where machines clear old bottlenecks and humans move on to interpretation and new questions. Others saw a credibility crisis coming for younger researchers, where access to compute and proprietary models matters more than individual insight, and where human verification becomes the remaining bottleneck. The result was a thread that largely accepted the achievements as real signals while refusing to accept OpenAI's framing at face value.
openai.com