I think it's likely that axiomatic approaches, and formal approaches will continue to produce interesting results and have some effect on regular mathematics.
But this is very different to suggesting that most regular mathematics will switch to using formal proofs. There's a big ergonomics gap at the moment.
An analogy could be to look how pure mathematicians look down on applied mathematicians' work, the applied mathematicians don't care, they just get on with their own standards. You need regular mathematicians to choose to switch over en masse, what will compel them to do that?
But this is very different to suggesting that most regular mathematics will switch to using formal proofs. There's a big ergonomics gap at the moment.
An analogy could be to look how pure mathematicians look down on applied mathematicians' work, the applied mathematicians don't care, they just get on with their own standards. You need regular mathematicians to choose to switch over en masse, what will compel them to do that?