GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]

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.