Force a large regular induced subgraph: does $F(n)/\log n\to\infty$? (Erdős #82)

For a graph on $n$ vertices, call an induced subgraph regular if every one of its vertices has the same degree inside the subgraph (empty and complete induced subgraphs count as trivial regular subgraphs). Let $F(n)$ be the largest integer such that every graph on $n$ vertices contains a regular induced subgraph on at least $F(n)$ vertices. Prove that $$F(n)/\log n\to\infty$$ as $n\to\infty$. Equivalently, letting $G(m)$ be the least integer such that every graph on $G(m)$ vertices contains a regular induced subgraph on at least $m$ vertices, show that $G(m)\le 2^{o(m)}$.

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred — a formalisation stub already exists — else a full written proof) that $F(n)/\log n\to\infty$, equivalently $G(m)\le 2^{o(m)}$; OR a disproof, i.e. a construction plus proof that $F(n)\ll\log n$ along some subsequence. ADVANCES: prove a lower bound $F(n)\ge g(n)\log n$ with $g(n)\to\infty$ on an explicit graph family, strictly beyond the Ramsey guarantee $F(n)\gg\log n$ stated in the background, with proof; OR establish a new exact value or improved bound for $G(m)$ beyond the records in the background ($G(5)=17$, $G(6)\ge21$, $G(7)\ge30$, $G(k)\ge\frac{9}{163}k^2$), delivered as an explicit extremal graph together with a machine-verifiable exhaustiveness certificate; OR tighten the general upper bound below $F(n)\ll n^{1/2}$ with proof. Deliver the proof file, or the extremal graph plus verified search code, or the improved-bound proof.