When you accept axioms randomly and reject even logical semantics, you wind up working with something like the so-called rado graph of Erdos. Call the first set of assumptions/structure meaningless and choose a new one, also having no grounding in reason - it turns out that would make no difference. "Almost certainly" you wind up with the same structure (the rado graph) in any case.
https://en.wikipedia.org/wiki/Rado_graph
So you can reject meaning (identifying the axioms with simple labels 1, 2, 3, ...) and truth (interpreting logical relations arbitrarily), but in doing so you ironically restrict mathematics to the study of a single highly constrained system.
I only disagree somewhat though - it is all contingent. We do say something like
IF { group axioms } THEN { group theory }
In the previous century there was an attempt to identify mathematics with formalism, but it defeated itself. We need to see truth in these systems - not individual axioms per se, but in systems composed from them. This is justified by the body of mathematics itself, to the non-formalist, the richness of which (by and large) comes from discoveries predating that movement.
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.
Rado has many interesting subgraphs, for example the implication graph of every countable theory. Are arithmetic propositions associated randomly? Not as we see it, but in some sense they could be (even iid). It is not the quite the same but I take the rado construction to be the logical extreme of the position there is no inherent/meaningful truth in such theories. You need to deal with this kind of many-worlds absurdity that falls out.
From your reply though I feel we are not really disagreeing so much. There is a kind of truth which is not propositional or self-evident but teleological. That is a sense in which I think the assigned truth values are meaningful.
The formalist movement was indispensable, I shouldn't have implied it was merely self-defeating. But I believe the philosophy that mathematics is fundamentally arbitrary mechanical symbol manipulation is wrong.