This talk introduces a coinductive perspective on provability, where proofs are not restricted to finite trees but may instead take the form of finite graphs or, more generally, non-wellfounded trees. Focusing on the linear-time μ-calculus, we present a sound and complete cyclic axiomatisation and demonstrate its use in establishing the interpolation property for the logic. We further show how this approach provides an insightful route to proving the completeness of the finitary axiomatisation. This work is part of a broader collaboration with Graham E. Leigh aimed at streamlining soundness and completeness proofs for modal and temporal logics.