$L^2$-Betti numbers and computability of reals

We study the computability degree of real numbers arising as $L^2$-Betti numbers or $L^2$-torsion of groups, parametrised over the Turing degree of the word problem. Moreover, we explain how such considerations can be modelled in a proof assistant.