By Section 5.5 in Tenenbaum: Introduction to analytic and probabilistic number theory, we know there exists an explicit constant $C>0$ such that $$\sigma(n)\leq e^\gamma n\log\log n+C n,\qquad n\geq 3.$$ 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{C}{e^\gamma\log\log n}\right)\exp(H_n)\log(H_n),\qquad n\geq 3.$$ 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 (of course most of us believe it is decidable).