To be honest, when I read e.g. Haskell code, I don't get the sense of a mathematical proof at all, not compared to proof assistants like Isabelle/HOL, Coq, or Lean. It looks more like abstract, high-level wizardry, casting that transform the output of one function into the correct type so that it can become input into another; and yet it's very abstract typing, nothing like proof-assistant tactics (though I admit I'm not all that experienced with proof assistants either).

I think immutability is more about making it easier to reason about the code than mathematical proofs specifically.