7
Uniformly random $k^2$-vertex graphs have clique size $O(\log k)$, well under $k$, and independent set size also $O(\log k)$, implying that their chromatic number is $\Omega(k^2/\log k)$.
As for $k^2$-vertex triangle-free graphs, their chromatic number can be $\Theta(k/\sqrt{\log k})$ (and not higher); see Kim, Jeong Han (1995),
"The Ramsey number $R(3,t)$ ...
5
Compactness for FOL was done in HOL by John Harrison, and reported at TPHOLs 1998. See Formalizing basic first order model theory.
1
If LOGLOG = NLOGLOG then LOG = NLOG. See more in:
https://www.sciencedirect.com/science/article/pii/0304397590900086
and therefore, your question is still an unsolved problem.
Only top voted, non community-wiki answers of a minimum length are eligible
