  We study the computational expressivity of proof systems with fixed point
operators, within the `proofs-as-programs' paradigm. We start with a calculus
$\mu\mathsf{LJ}$ (due to Clairambault) that extends intuitionistic logic by
least and greatest positive fixed points. Based in the sequent calculus,
$\mu\mathsf{LJ}$ admits a standard extension to a `circular' calculus
$\mathsf{C}\mu\mathsf{LJ}$.
  Our main result is that, perhaps surprisingly, both $\mu\mathsf{LJ}$ and
$\mathsf{C}\mu\mathsf{LJ}$ represent the same first-order functions: those
provably total in $\Pi^1_2$-$\mathsf{CA}_0$, a subsystem of second-order
arithmetic beyond the `big five' of reverse mathematics and one of the
strongest theories for which we have an ordinal analysis (due to Rathjen). This
solves various questions in the literature on the computational strength of
(circular) proof systems with fixed points.
  For the lower bound we give a realisability interpretation from an extension
of Peano Arithmetic by fixed points that has been shown to be arithmetically
equivalent to $\Pi^1_2$-$\mathsf{CA}_0$ (due to M\"ollerfeld). For the upper
bound we construct a novel computability model in order to give a totality
argument for circular proofs with fixed points. In fact we formalise this
argument itself within $\Pi^1_2$-$\mathsf{CA}_0$ in order to obtain the tight
bounds we are after.
  Along the way we develop some novel reverse mathematics for the
Knaster-Tarski fixed point theorem.
