The notion that mathematics would be over just because it's slightly easier to find proofs is like the idea that astronomy would be over because of telescopes.
Maaaybe.
On the other hand, proofs was the main thing that distinguished good mathemeticians. It was the way of sorting out who should be a math professor.
It's probably a bit of a blow for math professors. For almost everyone down the "food chain" though - who cares? I'd argue that mathematical thinking is still very useful, even if you offload the heavy lifting to power tools. Math teachers still need to exist. Math tests probably still make sense - you want to incentivise learning, and test to see who the brightest or most studious students are. Math will still be used for physics, economics, etc - no one actually cared about most of the new proofs anyway, it was just a fun tournament to pick math professors with a side effect of generating a bit new knowledge.
At some point, maybe humans don't need to make decisions. We can just sit in VR racks being fed and entertained by AI like we're in The Matrix or Wall-E, as they fill some age-old instruction to make the humans happy and healthy. But until then, humans still need to make decisions, and mathematical thinking makes us better at that.
Kind of an odd statement to make. The ICCF (international correspondence chess federation) lost a good chunk of players but still maintains a decent base of active players. There's also many orders of magnitude more playing correspondence chess in local federations or on online sites which all offer correspondence like time controls.
Computers definitely changed it, because now the best players are simply those who are best at dealing with chess engines, but it's still very much alive. The games played there also regularly studied by high level over-the-board players because it provides as close as we can currently get to the objective assessment of things like openings.
For instance it's extremely interesting to see things like the fact that the King's Indian Defense does okay in correspondence in spite of all engines insisting white has a practically decisive edge after about 10 moves in most lines.
---
Of course there's an interesting nuance that 'back in the day' a good correspondence player was almost certainly a good chess player. Whereas now a days its a different skillset altogether. The currently top rated correspondence player is a 20 year old who started playing correspondence 2 years ago, with no title and no rating in normal chess.
And I think we may see something similar in math. I'd wager that, at least in the longrun, the skill set required to effectively apply LLMs to mathematics may have less overlap than would be expected with the skillset to make progress in mathematics in the 'traditional' way.
I sketch, really badly, and I enjoy the process of doing that. The fact that an AI can make a better picture is irrelevant. Photography can do the same. I still enjoy sketching.
But I don't have to make my living from sketching. If I did, I would be more concerned and looking at how that changes.
I can see how both things can be true: mathematics is not "over", but professional mathematicians are looking at the skillset that they have carefully cultivated over their career and realised that those skills are probably not what will serve them best in the years to come. Tomorrow's mathematicians are not probably not going to be the same sort of people as today's mathematicians.
Same as us software devs. Software development isn't "over", by any means, but Software Development as a profession is changing extremely rapidly and the skills that got us this far are probably not the ones we need for the next decade.
RSI will mean that you'll be in the VR rack sooner than you might think, assuming we unlock the good ending.
The change happening now is already significant and isn't slowing.
I am not predicting anything, but it would not be surprising if in 10 years (or less) machines were pushing mathematics forward at a rate that left mathematicians the role of finding ways to translate results to other humans. And it wouldn't be surprising if machines were better at that than mathematicians too.
The faster things go, the more people's horizons seem to shrink. Things are moving fast enough that nobody on Earth knows what 10 years from now will look like.
There may be a finite point at which we've proven and codified everything but the most inane meta-meta-meta-maths though.
It's more of a theoretical corpus for the sake of this discussion. Just think of it as "all math humans have discovered/invented".
> Are all theorems or axioms useful?
Definitively no! Check out the first incompleteness theorem proof by diagonalization. The whole proof is based around generating new "facts" that are completely useless and uninteresting, outside of their utility in the proof itself.
It's actually a great question: to what extent do the incompleteness theorems actually apply to stuff that isn't silly and useless! The same goes for a couple similar proofs in other domains. An important one in Computer Science is Turing's proof that the halting problem can't be solved. There's at least one other important proof that is similar but I can't remember it at the moment.
To massively oversimplify, they can be boiled down to variations of:
> This statement is false.
Which proves that allowing self-referential statements can create a statement that isn't true or false. But they all raise the question: how often does this actually happen with statements we actually care about?
Observational astronomy is the most easily automated field, survey telescopes already scan the skies by automatic schedules.
https://rubinobservatory.org/explore/how-rubin-works/lsst/ca...