> where techniques not known to the researcher are available and profitably employed - ai brings them into the fray fast - and someone with experience immediately sees where to go with it
> So far AI still doesn't make definitions. It tries but it doesn't really see structure - only patterns on which it can impose (by brute force) known structures.
Insightful and nicely phrased!
Mathematicians are victims of their own success, by systematizing Formalism which made AI possible in the first place.
Paradoxically, they should also be indicted for removing the Human element by deemphasizing the study of Philosophy of Mathematics (i.e. ontology/epistemology/discovery/invention) and its mapping to Reality, but focusing only on formalization as an end in itself.
As you point out, the "definitions" (i.e. conceptual theory) are what is the critical aspect of discovering/inventing/doing mathematics and this has been forgotten in mathematics education since the Formalists gained ascendancy.
I think it is time to go back to the foundations of Mathematics and its Teaching viz. various types of Logical Reasoning, discovered/invented structures and their relationships based on Reality (the ontology and epistemology), with the final goal of understanding Nature itself.