Reminds me of the following papers (from 1979!) by Ernst Snapper;

1) What is Mathematics? - https://sci-hub.reatk.com/10.2307/2320582

2) The Three Crises in Mathematics: Logicism, Intuitionism and Formalism - https://sci-hub.reatk.com/10.2307/2689412

AI is the fourth crisis in Mathematics!

Formalism has been so successful that the General Public thinks that is all there is to Mathematics. And now AI has made this trivial.

But hopefully, Mathematicians are looking at more foundational and philosophical underpinnings.

The thing is that logicism and formalism were both essentially successful - Godel might thrown a wrench into Hilbert's plans but correcting for the incompleteness problem, a formal process can go forward. Intuitionism was a failure in the sense that just the existence of computers shows

The thing is, I think mathematics as a whole has reached a bit of the sort of crisis that mathematical foundations reached after Godel's theorem. I think Raymond Smullyan said something like (paraphrasing)"We know the continuum hypothesis is independent, it can't be proven or disproven by other hypotheses, we're not trying to do that. But if it can be stated in such a way that it is as intuitively clear as the other other axioms of set theory, then it will likely be accepted".

Mathematicians now can cruise through a huge area of "what can be mechanically deduced/mechanically constructed" and it seems like the task becomes highlighting what matters to us (as humans or mathematicians or some community) within that realm.