Can AI Prove Mathematical Conjectures? The Truth Behind the GPT-5.6 Incident and the Limits of Large Language Models

A Rumor That Shook the Math Community

Recently, a PDF titled GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture sparked heated discussion on Hacker News, quickly gathering 125 upvotes and over 110 comments. The document claimed that a certain version of OpenAI's model (GPT-5.6 Sol Ultra) had successfully produced a complete proof of the famous Cycle Double Cover Conjecture (CDC) in graph theory.

If true, this would be a landmark breakthrough for AI in pure mathematics. However, as the community discussion revealed, the matter is far less straightforward than the title suggests. This article starts from this incident, untangles the technical truth behind it, and explores the true capability boundaries of large language models when it comes to mathematical proofs.

What Exactly Is the Cycle Double Cover Conjecture

A Classic Unsolved Problem

The Cycle Double Cover Conjecture was independently proposed by Seymour and Szekeres in the 1970s and is one of the most famous unsolved problems in graph theory. Notably, Paul Seymour is a giant in the field of graph theory. Together with Robertson, Sanders, and Thomas, he produced the second computer-assisted proof of the Four Color Theorem in 1997, and was deeply involved in laying the foundations of Graph Minor Theory—the Robertson-Seymour theorem itself being one of the most profound achievements in 20th-century graph theory. The CDC conjecture emerged from the very outset within the sights of top mathematicians, which speaks to its difficulty.

Its core proposition is roughly this: for any bridgeless connected graph, there exists a family of cycles such that every edge in the graph is covered exactly twice by these cycles.

To understand the depth of this proposition, one must understand the meaning of "cycle" and "cover" in graph theory. A "cycle" in graph theory refers to a path whose start and end points coincide and which does not repeat any vertex, while a "cover" requires that every edge in the graph be included in at least one cycle. The CDC conjecture requires every edge to be covered exactly twice, and this "exactly twice" symmetry requirement makes the problem extremely subtle. Similar to the Four Color Theorem, the CDC conjecture is stated with extreme simplicity, yet corresponds to deep combinatorial and topological constraints—this "easy to state, hard to prove" property is a common characteristic of top-tier graph theory problems.

Simple as the statement appears, it has resisted the efforts of mathematicians for nearly half a century. The difficulty of the CDC conjecture is rooted in the deep structure of graph theory. A "bridgeless connected graph" is one that remains connected after the removal of any single edge; the presence of a bridge makes it impossible for the covering structure to satisfy the symmetry requirement.

The CDC conjecture is closely related to the study of the Petersen Graph and the Snark family of graphs—a connection worth elaborating on. The Petersen graph is one of the most important "counterexample graphs" in graph theory. Constructed in 1898, it has only 10 vertices and 15 edges, yet on a minimal scale it exhibits prototypes of nearly all the "hard properties" in graph theory. The Snark family is a generalization of the Petersen graph: they are cubic (each vertex connects to exactly three edges), connected bridgeless graphs with edge chromatic number 4 (meaning it is impossible to color all edges with three colors such that adjacent edges differ). Mathematicians have proven that if the CDC conjecture holds for all Snark graphs, it automatically holds for all bridgeless connected graphs. The existence of Snark graphs is precisely why the CDC conjecture is so difficult to break through by induction—there are known to be infinitely many Snark graphs, making exhaustive verification impossible, and the Snark family thus constitutes the "hardest core" of the conjecture.

Moreover, the CDC conjecture has a deep connection to surface embedding theory in topological graph theory, a connection that reveals the deeper mathematical significance of the conjecture. For any graph embedded on an orientable surface (such as a sphere or torus), its face boundaries naturally form a cycle double cover—each edge belongs to exactly two face boundaries. This observation transforms the CDC conjecture into a profound question: is every bridgeless connected graph structurally equivalent to some orientable surface embedding graph? If this equivalence holds, it means that discrete combinatorial structures can be fully captured by continuous topological structures—a concrete manifestation of the grand mathematical theme of "the unity of the discrete and the continuous." Therefore, the conjecture essentially asks whether a topological structure can be characterized algebraically. It is deeply connected to many important structures in graph theory—Snark graphs, the Four Color Theorem, embedding theory—and to this day it remains a recognized open conjecture, with no complete proof accepted by the mathematical community.

Why It Is So Hard to Prove

Precisely because the CDC conjecture has never been cracked by human mathematicians, any claim of a "complete proof" should be subjected to the strictest scrutiny. The bar for verifying a mathematical proof is extremely high—it is not enough for the logic to "look coherent"; every step of the derivation must withstand formal verification. The computer-assisted proof of the Four Color Theorem (1976) once inspired brief optimism, yet no similar breakthrough has occurred for the CDC to date. History is full of proof attempts that appeared rigorous but harbored fatal flaws, ultimately failing in peer review.

A famous cautionary example is the history of Fermat's Last Theorem before 1995: the first version of the proof Wiles submitted in 1993 was found to contain a serious flaw concerning Euler systems, and it took him over a year, working jointly with his student Taylor, to repair it. This shows that even proofs by top mathematicians can hide fatal defects beneath a seemingly rigorous exterior—let alone the outputs of an LLM.

The Community's Skepticism and the Truth of the Incident

Most Likely a Hoax or an AI Hallucination

Judging from the atmosphere of the Hacker News comments, the community's mainstream judgment on this document was highly skeptical, even directly deeming it a joke or a product of AI hallucination. Several key points of suspicion are worth noting:

The model name itself is a giveaway. "GPT-5.6 Sol Ultra" does not conform to any of OpenAI's official naming conventions and carries an obvious mocking flavor. The mode of dissemination is also seriously improper. If an AI had truly proven a mathematical conjecture that had remained unsolved for half a century, it would be a major event requiring peer review in top journals and repeated verification by multiple mathematicians—it would never first appear as an anonymous PDF circulating on a forum.

The more fundamental issue is this: the "mathematical proofs" generated by large language models have structural defects, rooted in the statistical nature of LLMs. Large language models learn the conditional probability distribution of token sequences through self-supervised pretraining on massive amounts of text; they are essentially statistical compression models. In mathematical reasoning scenarios, what the model learns is the "language patterns of valid mathematical text," not the "judgment of the validity of logical derivations." The crucial mismatch is this: an incorrect proof can completely overlap, at the linguistic level, with the distribution of a correct proof, and the model cannot distinguish the two through statistical features. This leads the model to tend toward generating output that is "statistically most like a correct proof" rather than a proof that is "truly valid logically." The deeper problem is: for top-tier unsolved conjectures, no text of a correct proof exists in the training corpus at all; the model can only rely on "interpolation" and "extrapolation" over related mathematical subfields, and mathematical reasoning is extremely sensitive to tiny logical errors—a single incorrect lemma citation can collapse the entire proof structure, yet still appear smooth and self-consistent at the linguistic level.

This leads to several typical failure modes: first, "lemma fabrication"—the model cites theorems that do not actually exist or whose content has been altered; second, "step-skipping hallucination"—omitting key steps in complex reasoning chains while covering them up with phrasing like "it is obvious that"; third, "structural mimicry"—the generated proof is highly professional in formatting and terminology, but the logical relationships are actually circular reasoning. For top-tier unsolved conjectures, there is no reference to a correct proof in the training data at all, and the model can only perform high-risk "extrapolation" outside the distribution, with the risk of hallucination rising exponentially. This is exactly the typical manifestation of AI hallucination in mathematical scenarios, and it explains why a model might fabricate lemmas, skip key steps, or formally imitate proof structures while lacking substantive content.

The Absence of Formal Verification Is the Core Suspicion

A truly credible AI mathematical proof usually needs to be machine-verified with a formal proof system (such as Lean, Coq, or Isabelle). The underlying foundation of such systems is Martin-Löf Type Theory, whose core idea comes from the famous Curry-Howard correspondence—each mathematical proposition is represented as a "type," and the proof of that proposition is a "value" of that type. The prover needs to write every step of the derivation as formal code, and the system automatically checks whether the types match at compile time. Any logical flaw causes the type check to fail, equivalent to a compilation error, fundamentally eliminating hallucination. The reliability of this mechanism has been validated by history: in 2005, Gonthier's team completed a full formalization of the Four Color Theorem in Coq, completely eliminating the uncertainty in the original 1976 computer-assisted proof, which required manual review of about 1,500 configurations, and transforming the verification process into fully mechanized computation. Lean's mathematics library, Mathlib, currently contains over 150,000 machine-verified theorems, providing AI with a reliable knowledge base.

DeepMind's AlphaProof (2024) uses Lean 4 as its verification environment, deeply integrating a large language model with a formal system. Its architecture borrows from AlphaGo's Monte Carlo Tree Search framework: the model replaces the "board state" with a "proof state," selecting a proof tactic each time, and Lean immediately returns binary feedback on whether the step is valid—successful steps advance the proof tree toward the goal, while failures trigger backtracking. The core advantage of this "generate-verify" closed loop lies in the absolute reliability of the reward signal: the validity of a mathematical proof step is as objective as the outcome of a Go game, with no gray area, fundamentally avoiding the failure mode of a language model where "sounding correct" leads to acceptance. In recent years, tools of this kind are the serious direction for AI-assisted mathematical research—the proofs they generate can be checked step by step by a computer, fundamentally eliminating hallucination.

A natural-language "proof" produced purely by an LLM, if it has not undergone formal verification, has almost zero credibility. This is precisely the most central point of suspicion in the GPT-5.6 incident.

Can AI Really Do Mathematical Proofs?

The Long Road from Assistive Tool to Autonomous Reasoning

Setting aside this specific incident, AI's real progress in mathematics itself deserves serious consideration. DeepMind's AlphaProof and AlphaGeometry 2 have reached silver-medal level at the International Mathematical Olympiad (IMO), able to solve fairly difficult competition problems. The common feature of such systems is: the deep integration of the intuitive capability of neural networks with the rigor of symbolic reasoning engines.

But we must soberly recognize that there is an essential gap between IMO competition problems and unsolved world-class conjectures. IMO problems are designed under strict constraints: the problem must be solvable within the framework of secondary-school mathematics, the boundaries of knowledge required to solve it are clear, and the problem committee already possesses a standard solution. This means AI's success on the IMO is essentially a "bounded search problem"—finding a path within a known toolset. More critically, IMO problems already have known answers and verification paths when they are set, and the AI system is essentially searching within a "reachable solution space."

World-class unsolved conjectures (such as the CDC conjecture, the Riemann Hypothesis, or P vs NP) are exactly the opposite—they often require inventing entirely new mathematical objects or frameworks, requiring the creative expansion of the representation space of mathematics itself, rather than searching within an existing space. When Wiles proved Fermat's Last Theorem (1995), he introduced a profound connection between modular forms and elliptic curves; when Perelman proved the Poincaré Conjecture, he invented the technique of Ricci flow with surgery—these were genuine acts of mathematical creation, not the recombination of existing tools. Wiles's core breakthrough was proving the semistable case of the Taniyama-Shimura conjecture, and this connection itself had long been invisible in the historical study of Fermat's Last Theorem—a genuine act of mathematical creation. Many breakthroughs in history took years or even decades, and drew upon mathematical tools that at the time had no known connection to the conjecture.

The success of current AI systems on the IMO mainly relies on efficient search and combination over existing mathematical structures, rather than creatively opening up new fields. This capability is still separated by an essential methodological chasm from independently cracking a conjecture at the level of the CDC. No AI system currently demonstrates the ability to independently crack top-tier unsolved conjectures.

It is worth mentioning that in 2023, another project under DeepMind released an interesting positive case: an AI system discovered a Cap Set construction in combinatorics that surpassed the best known human lower bound, published in Nature. But the nature of this result is "discovering, within a known framework, a construction humans had overlooked"—still a challenge of a different order of magnitude from "independently creating a new mathematical framework to prove an unsolved conjecture."

Where Are the Capability Boundaries of Large Models

The genuine strengths of general-purpose large language models (such as the GPT series) in mathematical scenarios include:

Summarizing and organizing existing knowledge, helping researchers quickly digest the literature
Providing preliminary inspiration for proof approaches, serving as a brainstorming partner
Assisting with formalization translation, converting natural-language proof drafts into languages like Lean

Their weaknesses are equally clear: they cannot self-verify logical correctness, they easily accumulate errors over long reasoning chains, and they lack the ability to judge "what constitutes a genuinely novel mathematical idea." Treating an LLM as a black box that can "prove conjectures with one click" is a serious misjudgment of current technical capabilities.

The Lessons Behind the Incident

This GPT-5.6 incident, whether a hoax or a misreport, reflects a widespread impetuousness in current AI discussions. Against the backdrop of AI's rapidly evolving capabilities, people are prone both to excessive deification and to losing their bearings in a stream of information that is hard to distinguish as true or false.

For tech practitioners and general readers alike, this incident reminds us to hold fast to three basic principles of judgment: extraordinary claims require extraordinary evidence, especially in a field like mathematics that tolerates not the slightest ambiguity; formal verification is the watershed for measuring the credibility of AI mathematical achievements; and view AI's capability boundaries rationally, neither blindly hyping nor wholesale dismissing.

What truly deserves continued attention is the serious research direction of deeply integrating AI with formal systems, exemplified by AlphaProof. They may not appear under sensational headlines like "proving a century-old problem overnight," but they are steadily driving real progress in AI-assisted mathematical research. When one day an AI truly cracks a major conjecture, it will surely be an achievement that has been repeatedly verified and jointly recognized by the mathematical community—not an anonymous PDF circulating on a forum.