Sharing AI Progress in Mathematics

Commenters debated OpenAI’s release of many claimed mathematical results produced with models and formalized on GitHub. Some commenters marveled at the scope and surprise of particular claims - Unique Games, matrix multiplication exponent improvements, FFT faster than O(n log n), Barnette’s Conjecture, Riemann-related gains - and pointed to the provided Lean proofs and reasoning traces as fascinating evidence of real progress. Several praised public sharing over gatekeeping, suggested these outputs could accelerate math by decades, and hoped the results would enter future training data; others highlighted the accessibility of the repositories and the detailed traces as useful for follow-up.

Opposing voices stressed verification, attribution, and social impact. Many commenters warned that broad, high‑impact claims demand careful spot checks by domain experts and urged human reviewers’ names on papers; some predicted errors or formulation mistakes despite Lean files. Others questioned OpenAI’s decision to test advanced math on proprietary models against advisory group advice and worried about effects on PhD work and academic credit. A few framed the work as startling evidence of rapid AI capability gains, while skeptics labeled some outputs as token prediction or “stochastic parrots,” insisting rigor and community validation are the real tests.