GPT-5.6 used a prompt to close a 30-year gap in convex optimization
An AI model (GPT‑5.6 “Sol Pro”) has helped prove a 30‑year‑old open result in convex optimization, using a ten-page, expert-crafted prompt and a proof later verified in the Lean theorem prover. Commenters debate how much genuine novelty the system contributed versus acting as an extremely powerful automated assistant, and what this implies for the future role of mathematicians and programmers, especially on “low‑ and medium‑hanging fruit” problems. The thread widens into questions about whether large language models are merely “stochastic parrots,” how quickly they might displace human work across fields, and what kinds of social and economic changes would be needed if AI continues to advance.
Scope of the result and how it was obtained
- Commenters note the proof is Lean-verified but not yet peer reviewed, so its status is “promising but provisional.”
- The key nuance: GPT‑5.6 Sol Pro used a ~10‑page, domain‑expert prompt built on a year of prior human work (including earlier LLM-assisted attempts).
- This is seen as strong evidence that LLMs can close gaps when the path is reachable with existing techniques, but not “type ‘solve this’ and walk away” autonomy.
Implications for math and research careers
- Some argue low- and “medium-hanging fruit” in math/TCS will increasingly be offloaded to AI, leaving humans to focus on truly novel ideas and problem selection.
- Others worry this undermines traditional training paths, where juniors cut their teeth on such problems.
- Several compare this to software: juniors and “recipe-followers” may be displaced first; deep domain and systems-level understanding still matter.
LLMs: intelligence, creativity, and “stochastic parrot” debate
- Enthusiasts say solving 30‑year problems and contributing to other conjectures refutes the “mere parrot” view and shows genuine reasoning.
- Skeptics maintain LLMs are sophisticated prediction engines built on human-generated patterns, not truly creative or understanding.
- Some suggest that if this isn’t “intelligence,” the word loses meaning; others reply that statistical pattern-matching plus brute-force search can explain it.
Prompting, agents, and “harness engineering”
- Multiple comments stress that writing good prompts and processes is closer to process/harness engineering than “magic prompting.”
- There is discussion of multi-agent systems (Pro vs Ultra), where models plan, execute, test, and self-critique in loops.
- People note LLMs can also help generate their own prompts and workflows, reducing the need for manual prompt craft over time.
Formal verification and proof infrastructure
- Lean is highlighted as today’s analogue of older systems like Mizar; machine-checked proofs are seen as crucial for trusting AI-generated math.
- Some would like to see LLMs tackle very long or opaque proofs (e.g., large classification theorems) via full formalization.
Broader societal and economic concerns
- Reactions range from excitement (“intelligence is cheap, we can accelerate science”) to anxiety about job loss, stratification, and “technofeudal” futures.
- Several argue the real problem is political economy: how gains are distributed, not the math itself.