OpenAI, the Partition Principle, and Mathematics
OpenAI’s release of hundreds of AI-generated proofs for difficult open math problems, many backed by Lean formal verification but written in opaque, awkward prose, is polarizing the mathematics community. Critics argue the company is using math as a PR vehicle, offloading the labor of verification and exposition onto already overstretched researchers while undermining established norms of clarity, attribution, and scientific process. Supporters counter that formally verified results are inherently valuable, can be refined over time, and may accelerate mathematical progress even if the initial outputs are messy and hard to understand.
Burden on mathematicians and “AI slop”
- Many see the dump of hundreds of partially incomprehensible AI-generated proofs as a denial-of-service attack on experts: a small group of people with the right skills are inundated with artifacts they are socially and professionally pressured to assess.
- Others argue “no one is forced” to read them; critics reply that grants, publicity, and constant inquiries from colleagues/students make non‑engagement costly in practice.
Validity and Lean formalization
- One side claims that Lean-verified proofs whose formal statements match the target problem are among the most reliable mathematical results.
- Counterpoints note concrete failures: a “disproof” of Collatz exploiting a Lean kernel bug, and retracted results with sign errors. Formal verification, specs, and code can all be wrong or mismatched.
- Several say reading the Lean statement is feasible, but the proof objects are huge and effectively unreadable.
Readability, exposition, and the nature of math
- A central complaint: the papers are unclear, oddly structured, and poorly cited; if submitted by humans, many would be desk-rejected.
- Mathematicians emphasize that math is not just truth-plus-certificate; exposition, new methods, and integration with existing theory are core scientific work.
- Others respond that many human papers are comparably bad, and that a true but ugly proof is still valuable, just less so than an understandable one.
OpenAI’s motives and release strategy
- Defenders frame the release as scientific openness and an evaluation tool; anyone interested can build on the results.
- Critics see primarily a PR stunt: using open problems to market capabilities, ignoring advisory recommendations (e.g., on attribution, failure rates, and improved exposition).
- Some call the process exploitative: community labor is needed to interpret and clean up results that primarily benefit the company. There are also worries about AI outputs closely mirroring user-submitted, unpublished work.
Impact on careers and incentives
- Researchers highlight opportunity cost and a brutal job market: time spent deciphering AI artifacts may not help careers, especially for students and non-tenured scholars.
- Others see a “buffet” of new results and lemmas as opportunities for ambitious mathematicians to refine, extend, and improve.
Future of math with AI
- Enthusiasts are excited: they point to active community projects improving AI-derived bounds, envision automated repositories of formal proofs, and expect future models to generate “enjoyable proofs.”
- Skeptics worry about a “loss of meaning”: humans relegated to debugging or translating alien proofs, fields refocused on verifying black-box results rather than developing shared understanding.