Ten advances in mathematics and theoretical computer science
OpenAI’s claim that an internal AI model has produced formal proofs for ten long‑standing problems in mathematics and theoretical computer science is prompting both admiration and skepticism. Commenters highlight how quickly AI capabilities in formal reasoning are advancing, while questioning the lack of methodological transparency, the true cost and generality of the results, and whether these are cherry‑picked successes. The thread repeatedly returns to deeper issues: what this means for the careers and status of human mathematicians, how to attribute authorship and credit for AI‑assisted proofs, and whether such systems move us meaningfully closer to artificial general intelligence or merely expose new limits.
Overall reaction to the AI math results
- Many see the results as historic: AI solving long‑open, nontrivial problems across several areas of math and TCS.
- Others emphasize they’re still “just 10 problems” and not Millenium‑level yet, so capabilities shouldn’t be over‑interpreted.
- Several commenters note that independent researchers using public models have also solved smaller Erdős‑type or OEIS problems.
Impact on mathematicians and careers
- Some are excited: more math, more tools, and a need for more humans to guide and interpret AI work.
- Others fear a “chess” scenario: a tiny elite thrives while thousands of working mathematicians lose career paths and credibility signals.
- There’s debate whether math exists “for human jobs” vs. “for human knowledge,” and whether the benefit justifies job losses.
Validity of proofs and Lean formalization
- Lean proofs are seen as strong but not magical: humans must still verify the formal statement matches the intended theorem.
- Concerns: kernel bugs, use of
sorry/cheats, and enormous machine‑generated Lean specs that are hard for humans to audit. - Recent Lean kernel issues (e.g., around a fake Collatz counterexample) are cited as cautionary examples.
Cost, cherry‑picking, and transparency
- OpenAI says token cost per problem was low (~$2k total), but many argue this ignores salaries and infrastructure.
- Commenters want full experimental details: how many problems were tried, failure rates, retries, and compute budgets.
- Some argue cherry‑picking doesn’t invalidate the theorems, but does matter for understanding current AI capability surfaces.
Authorship, tools, and credit
- Strong disagreement over whether AI is “just a tool” like a calculator or crane vs. a creative agent that deserves explicit credit.
- Many support OpenAI’s stance that claiming full human authorship on an AI‑generated proof is misleading.
- Analogies used: 3D printers, manufactured objects, calculators, and human–machine co‑production of designs.
Capabilities, limits, and future directions
- AI currently excels at proofs, counterexamples, bounds improvements, and grindy combinatorial work; “new theory” and big conceptual frameworks remain largely human.
- Some think current LLMs already “intuit” in ways non‑obvious to experts; others insist they’re still recombining existing methods.
- There is disagreement whether this trajectory implies rapid recursive self‑improvement and “FOOM,” or a more gradual, compute‑limited plateau.
Societal and economic implications
- Threads explore UBI, wealth concentration, and whether AI‑driven abundance will actually improve average lives vs. just profits.
- Concern that frontier labs pursue flashy math demos for hype while underinvesting in applied domains like climate, health, and materials.
- Many note intense emotional reactions: excitement, grief, denial, and “moving the goalposts” accusations on both pro‑ and anti‑AI sides.