Yes. This is how this works.

Any proof which is correct can be formalized. That is what is means for a proof to be correct.

I’m not sure why you are restricting the scope of our discussion to what _Lean_ can(not) formalize. Even if we do choose to do that for some reason, Lean is not a formal system of fixed axioms; it supports optional additional axioms.