It is known that (see Section 5.5 in Tenenbaum: Introduction to analytic and probabilistic number theory)
$$\sigma(n)\leq e^\gamma n\log\log n+O(n),$$
with an explicit implied constant. By Lemma 3.1 in Lagarias's paper, we also know that
$$\exp(H_n)\log(H_n)\geq e^\gamma n\log\log n,\qquad n\geq 3.$$
Combining these two estimates, we infer that
$$\sigma(n)\leq\left(1+\frac{O(1)}{\log\log n}\right)\exp(H_n)\log(H_n),$$
with an explicit implied constant. The fraction on the right hand side tends to zero (effectively), confirming the observation by the GCHQ Problem Solving Group.

The barrier to prove Lagarias's inequality is the same as the barrier to prove the Riemann Hypothesis, since these two statements are equivalent. It is a difficult problem, and perhaps it is even undecidable from the ZFC axioms.