Real talk.
AI solving these makes me feel like mathematicians put far more importance on their work than was actually there. Many solutions seems to be tautological games, and games of logic where conjecture puzzles that few work on or care can be solved by AI which doesn’t care what it works on.
It seems to always be some form of this:
Mathematician: “Propose conjecture a and conjecture b can’t be true simultaneously”
AI: “they can”
Everyone: “ok…”
I know this might be unfair or out of ignorance but it genuinely is how this field feels today. Games of games with self importance added in.
Edit: the point I should have made is, should we be using AI to figure out what proofs MATTER now vs games of proofs?
Academic math is a bit like basic research. You come up with funny ways to look at numbers or prove weird statements about this thing you came up with and call a "group", and a couple years or decades or centuries later it turns out that this solves real problems in electrical engineering or biology
Or it ends up never becoming useful. But you can't know that in advance
Look up how pure mathematics connects back to reality in countless unexpected and useful ways, time and time again.
To borrow a common wisdom about marketing, half of all mathematics is a waste of time, but you can't know which half.
We call a proof that is not tautological "wrong".
Very useful games, self-importance or no.
See pattern, conjecture generalization, test generalization. It's almost like empirical math. I like it and I also like mathematicians doing it the old way.
Don't do that...
"tautological games".
All proofs are a form of tautology, you have to end up back at the point your theorem proposed. Math is games of logic. That's what it is.