OpenAI withdraws three mathematical results
OpenAI’s mass release of AI-generated mathematics papers – followed by the quiet withdrawal of three results over errors – has triggered a clash between hype-driven AI research and traditional standards of mathematical rigor. Commenters argue over whether partially Lean-formalized proofs and unreadable, AI-written manuscripts should be shared early for community scrutiny or held back until thoroughly verified, given the heavy burden this places on human experts. Beneath that, many worry about the long‑term impact on the mathematical ecosystem itself: from funding and careers to the risk of flooding the field with hard‑to‑verify “slop” that may slow, rather than accelerate, genuine progress.
Release & Withdrawals
- OpenAI released ~700 math results (from ~4,000 problems) in a GitHub “preprint” dump; later withdrew three manuscripts after errors (e.g., a sign error) were found, and added several new Lean formalizations.
- Some see 3 withdrawn results out of hundreds as a normal scientific correction process; others argue it badly undercuts the headline claims.
Lean Formalization & Verification
- Around 40–42% of “top-line” results now have Lean formal proofs; some were added post-release.
- Many stress that Lean only guarantees the internal logic, not that the formalization matches the intended theorem. Errors can occur in:
- Misstating the problem in Lean.
- Using missing or subtly wrong definitions.
- Rare but real kernel bugs and “reward hacking” of proof assistants.
- Several note that many statements (e.g., standard conjectures) were already in math libraries; what’s new are the machine-generated proofs.
Quality, Readability, and “Slop”
- Multiple readers describe the papers as hard to read, poorly organized, and reference-heavy; “AI psychosis” and “slop” are recurring themes.
- There is concern that huge, opaque proofs are effectively unverifiable for humans, even if they digitally “check.”
Responsibilities, PR, and Incentives
- Critics say OpenAI rushed for hype/IPO optics, publishing unverified work and offloading verification onto the community.
- Defenders reply this is analogous to human preprints on arXiv, and that early release was explicitly requested by some mathematicians for transparency.
- Debate over whether OpenAI should have separated fully Lean-verified results from speculative ones, and whether they should pay external verifiers.
Impact on the Mathematical Community
- Fears that hype could:
- Undermine funding and careers in academic math.
- Turn mathematicians into unpaid proof-checkers for corporate models.
- Erode the “thriving community” needed to interpret and extend results.
- Others argue that if AI can automate large parts of math, that simply reflects economic reality; some welcome AI as a powerful new tool.
Parallels to Software & Other Fields
- Many compare this to LLM-generated code: massive productivity, but verification and maintenance become the bottleneck; “agent wranglers” replace traditional juniors.
- Broader worry that AI-generated “slop” will flood research (math, software, experimental science), shifting scarce human attention from creation to triage and cleanup.