Disproved. The site's label reads "DISPROVED (LEAN)"; its suffix is a catalog label explained under Formalization. The Statement quantifies over every graph $G$, and its answer is no. It fails trivially for forests: for $G=P_3$, the path with two edges, the $G$-free graphs are the matchings, $\mathrm{ex}(n;P_3)=\lfloor n/2\rfloor$, and there are $2^{(1/2+o(1))n\log_2 n}$ labeled matchings on $n$ vertices; for the stars $K_{1,k}$ with $k\ge4$ the bound fails even for unlabeled graphs. It also fails for a graph containing a cycle, by the status-defining source, Proposition 1.4 of Morris and Saxton (Adv. Math. 298 (2016), 534--580, refereed): there is a constant $c>0$ such that for infinitely many $n$ at least $2^{(1+c)\mathrm{ex}(n;C_6)}$ graphs on $n$ vertices contain no $C_6$. For non-bipartite $G$ the bound holds (Erdős, Frankl and Rödl 1986, Theorem 1.6). The claim pages are Morris and Saxton (full, accepted on the refereed publication and the curator's credit) and Erdős, Frankl and Rödl (partial, the non-bipartite case, accepted on the refereed publication); the 2026 Lean disproof in the lean-proofs repository declares itself a formalization of Morris and Saxton's proposition and is recorded on their page as a formalization link, which gives no formalized evidence.