> there exist constants C, X > 0 such that for every real number x > X, we have

>> log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cx.

These problems are only "uninteresting" to the extent that they can be "proven" by automated computation. So the interesting part of the problem is to write some completely formalized equivalent to a CAS (computer algebra system - think Mathematica or Maple, although these are not at all free from errors or bugs!) that might be able to dispatch these questions easily. Formalization systems can already simplify expressions in rings or fields (i.e. do routine school-level algebra), and answering some of these questions about limits or asymptotics is roughly comparable.