Are all systems of informal logic really just systems of formal logic that have not yet been understood mathematically?
It depends what you mean by "all systems of informal logic". If you mean all the ways people can reason, then your question is tantamount to asking if all human thinking can be formalized... and we simply don't know that. Even the lesser question whether all human thinking can be simulated by some machine is basically asking whether a strong AI can be built. (You can simulate what don't quite understand--for instance there's no deep way to understand an artificial neural network that [say] beats most people at Backgammon.)
If you mean just some system(s) of IL that people have (more or less vaguely) described... usually a FL based on that exists if the IL was interesting enough. (So take this as an experimental postulate.) Some 20th century examples (as the date of formalization): temporal & modal logic(s), paraconsistent logic(s) etc. The IL system may of course be flawed, but then it depends what is a logic, which is itself not a settled question even for the formal ones.