Mathematics is a formal system. The mathematician states axioms (that is, assumes the existence of some formal entities and relationships between them) and applies previously agreed formal inference rules to derive more relationships within the formal system.
Essentially, it's about making explicit the logical consequences that are implied by the original assumptions. Everything happens inside the formal system with no regard to anything outside that system. It's all about transforming meaningless symbols according to agreed rules that are concerned only with those symbols and not what they might correspond to outside that formal system.
In an applied problem, the mathematician maps elements of the external world to formal mathematical elements; mathematically manipulates the formal image of the external world to derive some implications; then inverse maps those formal implications back to the external world to make claims about implications in the external world.
The proofs in the formal systems are as proof-ish as any mathematics ever is. However, the external world and the mapping from the external world to the formal representation are not formal - so it seems to me that the proof in the formal representation are confined to that formal representation and can not extend back into the external world. That is, the chosen conceptualisation of the external world and the chosen mapping to its formal representation is assumed to be appropriate and the correctness of those assumptions is not able to be investigated from within the formal representation.
Consequently, I think the hardest part of applied maths for any problem domain would be finding a conceptualisation of the external world and mapping to the formal domain such that the formal manipulations actually tell us something about the external world, as a matter of fact. However, I don't see this discussed in the applied work that I read. The mappings are treated as self-evident.
This issue feels like it should be old-hat in the right literature. (It also feels a lot like the symbol grounding problem in #CognitiveScience.) I would greatly appreciate any pointers to literature with practical conclusions about this. (It also feels like something that #AppliedCategoryTheory people should have views about.)