GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
An OpenAI model, GPT‑5.6 Sol Ultra, is claimed to have produced a short proof of the long‑standing Cycle Double Cover Conjecture in graph theory, prompting both excitement and skepticism. Commenters focus on whether the proof has been independently verified or formalized in systems like Lean, how much orchestration, prompting, and trial‑and‑error were required, and what role human mathematicians played in selecting and validating the result. More broadly, the thread probes what this implies for the future of AI in mathematics—its current strengths in combinatorial problems, its limits in building new theories, and how such breakthroughs should be evaluated and trusted.
Proof validity and verification
- Many are excited but cautious: the proof is short, uses pre‑1990s graph theory, and looks plausible, yet could contain subtle errors.
- Some argue it should have been announced by professional mathematicians or after Lean formalization / journal peer review.
- Others note OpenAI has published a Lean formalization repo, but graph theory libraries are still immature, so mechanization is nontrivial.
- Several commenters tried to have other LLMs and tools check the proof; they generally report no obvious errors but stress this is not a substitute for expert review.
- At least one technical concern raised on Reddit is argued in-thread to be a notation issue, not a fatal flaw. Overall verdict: promising but not yet universally accepted.
Prompting, harness, and time awareness
- The released prompt is heavily meta: it instructs the model to assume a proof exists, work for at least 8 hours, avoid vague status reports, and explore multiple strategies.
- Commenters see this as “motivation hacking” and metaheuristic guidance rather than pure autonomy.
- There is discussion of time-tracking in agent harnesses (timestamps, OS
date, quota tools) versus models’ lack of innate temporal sense. - Sol Ultra is described as many parallel sub‑agents with max reasoning, differing from Sol Pro’s “best‑of‑N” approach.
Methodology opacity and survivorship bias
- Multiple commenters ask how many problems and prompt variants were tried, and how many failed runs preceded this success.
- Speculation that OpenAI has been running many problems since the earlier unit-distance result; absence of a “failure rate” makes it hard to gauge capability.
- Concern that companies will highlight rare successes for marketing while burying null results.
Significance for mathematics and proof assistants
- Some view this as a major milestone: an off‑the‑shelf model solving a famous open problem in under an hour.
- Others point out it’s a “clever trick” style proof, not a long, theory‑building breakthrough; they argue the next bar is autonomous development of substantial new theory.
- Strong support for moving toward Lean-style formal verification to cope with large volumes of AI‑generated proofs and reduce human checking bottlenecks.
Broader implications and anxieties
- Debate over which tasks are most automatable: anything with easily checkable correctness (math, code, security, some science) may be especially vulnerable.
- Philosophical discussion about the value of pure math, whether AI‑generated results “feel empty,” and what remains uniquely human (conjecture creation, taste, explanation, responsibility).
- Some express concern about jobs, human worth, and AI hype; others respond that human value isn’t tied to economic productivity and that tools will augment rather than erase people.