I am accepting and rejecting axioms _arbitrarily_ depending on application, but not _randomly_, and definitely not i.i.d. random.

The Rado graph you mentioned does look very interesting as a mathematical object in its own right! But it has approximately nothing to do with what we discussed, exactly because it requires i.i.d. randomness.

> Crucially, we then search for the right set of assumptions, and the conviction of modern science that there is a right set of assumptions is "effective" at least.

Well, multiple sets of assumptions can be 'right' or right enough, or perhaps no set can be. Eg as far as we can tell, no clever sets of axioms will allow us to predict chaotic motion, or predict whether a member of a sufficiently complicated class of computer programs will halt. (However, we can still be clever in other ways, and change the type of questions we are asking, and eg look for the statistical behaviour of ensembles of trajectories etc.)

> In the previous century there was an attempt to identify mathematics with formalism, but it defeated itself.

I say it was extraordinarily successful! It actually managed to answer many of the questions it set out at the start. Of course, many of them were answered in the negative. But just because we can now proof that every formalism has its limits, doesn't mean that informal methods are automatically limitless. Or that there is any metaphysical 'truth'.

The 20th century saw enormous progress in terms of thinking about formalism abstractly (that's the 'self-defeat' you mention, thanks to giants like Gödel and Turing). But it's only in the last few years that we've seen progress in terms of actually formalising big chunks of math that people actually care about outside of the novelty of formalisation itself.

Btw, just to be clear: IMHO formalisation is just one of the tools that mathematicians have in their arsenal. I don't think it's somehow fundamental, especially not in practice.

Often when you develop a new field of mathematics, you investigate lots of interesting and connected problems; and only once you have a good feel for the lay of the land, do you then look for elegant theoretical foundations and definitions and axioms.

Formalisation typically comes last, not first.

You try and pick the formal structure that allows you to make the kind of conclusions you already have in mind and have investigated informally. If the sensible axioms you picked clash with a theorem you have already established, it's just as likely that you rework your axiom as that you rework your proof or theorem.

That bidirectional approach is sometimes a bit hard to see, because textbooks are usually written to start from the axioms and definitions. They present a sanitised view.