How can we express "induction is the same as recursion", formally?

In a type system with propositions-as-types, such as Homotopy Type Theory (I will write what follows with that in mind) it is not something you would prove, but something that is built in.

Indeed in Homotopy Type Theory, the type of natural numbers, $\mathbb N$, is given ("freely") by $\mathbb N: \mathcal U, 0: \mathbb N, \mathrm{succ}: \mathbb{N\to N}$ and the following "recursion" principle (I'm using quotes here, because it is as relevant for recursion as it is for induction and since your question is specifically about the distinction between those two, one has to be careful) :

given a family of types $C: \mathbb N\to \mathcal U$, $p:C(0)$ and $f: \displaystyle\prod_{n:\mathbb N}(C(n)\to C(\mathrm{succ}(n))$, we have $rec(C,p,f): \displaystyle\prod_{n:\mathbb N} C(n)$, together with the following "rules" (defining equations) : $rec(C,p,f)(0) \equiv p$, $f(n)(rec(C,p,f)(n)) \equiv rec(C,p,f)(\mathrm{succ}(n))$

Now say you have a type $X$, $p:X$ and a map $h:\mathbb N\to X\to X$ and want to define a map $H:\mathbb N\to X$ such that $H(0)\equiv p$ and $H(\mathrm{succ}(n)) \equiv h(n)(H(n))$, then this recursion principle allows you to do that, by putting $C(n):\equiv X$ and $f(n):\equiv h(n)$, so it recovers what you seem to call recursion.

Now to recover induction say you have a proposition $P(n)$ that you want to prove by induction. But in this setting, $P(n)$ is a type a proving $P(n)$ is finding $p:P(n)$, so all in all you want an element of $\displaystyle\prod_{n:\mathbb N}P(n)$. Now if you have $p:P(0)$ (read "I have a proof of $P(0)$") and $f: \displaystyle\prod_{n:\mathbb N}(P(n)\to P(\mathrm{succ}(n))$ (read "I have a proof of $\forall n, P(n)\implies P(\mathrm{succ}(n))$"), then the induction principle gives you $q: \displaystyle\prod_{n:\mathbb N}P(n)$, that is, a proof of "$\forall n, P(n)$".

So in this context the two principles aren't just "formally similar" or "isomorphic", they're literally the same.

This can be seen category-theoretically as well. Say you have for simplicity a topos $T$ with a natural numbers object $N$, that is $N$ has a global element $0: 1\to N$, and a map $s: N\to N$ that have the obvious universal property. This universal property is literally what encodes recursion, but induction can be found from it too.

Indeed say you have a property $P$ on $N$, which really means (category-theoretically) a map $N\to \Omega$ ($\Omega$ being the subobject classifier). Then saying that "$P(0)$ holds" means essentially "the composite $1\overset{0}{\to} N \overset{P}{\to} \Omega$ is the $\mathrm{true}$ morphism".

Saying "for all $n$, $P(n)\implies P(s(n))$" can be interpreted as "the map $\{n:P\}\to N\overset{s}{\to} N$ factors through $\{n:P\}$" where $\{n:P\}\to N$ is the pullback of $\mathrm{true}: 1\to \Omega$ along $P:N\to \Omega$ (the subobject of $N$ defined by $P$).

This means that we have a commutative square $\require{AMScd} \begin{CD}\{n:P\} @>>> \{n: P\} \\ @VVV @VVV \\ N @>{s}>> N \end{CD}$ which can be extended with a triangle with $1\to N$ and $1\to \{n:P\}$

But now by the NNO property of $N$, this map $\{n:P\}\to N$ has a section (it is a section because the map to $N$ is unique) : however it was a monomorphism, therefore it having a section implies that it is an isomorphism, so $\{n:P\} = N$ and $N\overset{P}{\to} \Omega = N\overset{\mathrm{true}_N}\to \Omega$, in other words "for all $n:N, P(n)$", so we get back the induction principle as an easy corollary of the NNO-property, which is what defines recursion.

I don't know enough about topoi and specifically their internal language, but it is easy to see how the recursion principle can be found from the induction principle even set-theoretically, and I don't think one needs the law of excluded middle (although one may need some more assumptions on $N$, like that $0$ is not in the image of $\mathrm{succ}$, which doesn't follow from NNO-ness; these conditions would be needed to make sure for instance that $N$ is decidable even without the LEM) so there should be a way to do that internally to a topos, but someone with more knowledge should say something about that. If that's true (it definitely is in $\mathbf{Set}$ with LEM), then this shows that (in a topos) the two principles are again similar.

Unfortunately what I did was only give systems where the two principles are similar or can be derived from one another or are the same; I didn't answer the question of "how to state that they are somewhat isomorphic", so you'll have to tell me if that's fine by you !