The Simonovits product conjecture predicts a graph join structure for extremal graphs avoiding a fixed
finite family of forbidden graphs. Let 
be such a family and set 
, where 
is the chromatic number
of 
.
Write 
for the maximum number of edges in an 
-vertex graph containing no member
of 
as a subgraph, and 
for the number of edges
in the 
-partite
Turán graph.
The superlinear-surplus formulation assumes that, for some 
and 
,
 |
for all sufficiently large 
. The conjecture then asserts that every extremal
graph on sufficiently many vertices is a graph
join
 |
with each nonempty factor 
extremal for a fixed forbidden family 
whose minimum chromatic
number is 2. The sizes of the forbidden graphs in these
families are bounded by the largest size of a member of 
(Füredi and Simonovits 2013, Conjecture 2.8).
Xu (2026a) reported a finite family with 
and surplus of order at least 
for which an extremal
graph has connected graph
complement. Such a graph cannot be a graph
join of two nonempty factors. The construction would therefore refute the assertion
about every extremal graph, but does not alone
rule out the existence of other extremal graphs
that have the proposed form.
A weaker formulation asks only for the existence of one extremal graph that is a graph join of 
nonempty factors. Xu (2026b) separately reported a finite
family with 
and surplus of order at least 
for which every extremal
graph has a graph complement with at most
two connected components. A graph
join of three nonempty factors has a graph complement
with at least three connected components,
so this construction would also refute the weaker existence formulation.
Xu (2026a) reports a Lean formalization of the first construction and its extension to larger values of 
. Both papers credit GPT-5.6 Sol with the initial proof or
counterexample and manuscript, followed by author
verification and revision. As of Sep. 18, 2026, independent verification of
the Lean development and external specialist review of the complete results had not
been reported.
