Not sure why people are stopping at 'AI can do advanced math!' and calling that the field is gonna transform due to LLMs specifically. Pretty much any meta-formulation of math gives you some initial rules and a goal. From natural deduction and sequent calculus to dependent type theory and whatever flavour of category theory you choose, at a sufficiently abstract level, you'll end up with some form of search problem. ATP folks foresaw machines doing automatic proofing for decades, but it seems that noone had enough incentive in pursuing it at the cost of suffering the tediousness of the encoding process. Now AI labs took the opportunity to do something impressive and have shown that it's possible to close the ergonomics gap. But the deeper achievement is the decades of ATP and proof-assistant work that make machine-generated proofs mechanically certifiable in the first place.
I am pretty sure in the next couple of years we'll see more evolved sledgehammers [0], maybe with LLM-like tech playing a role in encoding theorems, that will allow us to prove deeper than we can do manually, then help with the archeology and extraction of learnings from observing the 'trace' of certified proofs. So instead of explore -> understand -> solve, we'll get solve -> compress -> understand.
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.
Or that chess is over because stockfish can easily beat any human player. Or that warehouses don't need workers now that we have forklifts.
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.
The process of creating mathematical proofs from scratch is itself a rather high form of art, so I personally care even though I’m not a mathematician, because I enjoy the cultural effects within science. A world without future inspiring stories like Yitang Zhang seems rather dull and gray in my view. And by the way, Stockfish did kill correspondence chess, the form of chess most similar to academic research, chess that was unproctored and untimed.
I think likely to be infinite, per Gödel's incompleteness theorems. Given a corpus of maths called A we can always find new unprovable axioms under A, giving us a new corpus. From there we can prove new theorems.
There may be a finite point at which we've proven and codified everything but the most inane meta-meta-meta-maths though.
That's now how it works. You generally can't know if a statement is provable/unprovable under A. In most cases, there's nothing to identify a new corpus.
This piece reminded me, of all things, of Gandhi's essay "Hind Swaraj." He was pretty anti-technological-driven change.
He was anti:
- Machinery replacing handicraft (skill disappeared and poverty followed)
- Labor-saving machines replacing human workers (workers became expendable)
- Doctors replacing consequences (people lost self-control)
- Railways replacing constraint and slowness (harm spread faster)
But he loved the sewing machine.
Gandhi’s test for whether to accept tech-driven change was whether it satisfied primary needs. Interpretation of those needs was certainly not universal. As he wrote: "...it is not the primary need of man to traverse distances with the rapidity of a motor car. The needle on the contrary happens to be an essential thing in life, a primary need.”
That's the airplane in this post. Excitement or fear of the AI airplane is either judged as helping mathematicians (sewing machine) or doing something not quite right (the above machinery/doctor/railway)...
Gandhi’s argument seems flawed. It’s arbitrary to decide the needle is a primary need because it requires delineation of need vs. want. If we took a time machine back every 100 years, that delineation would be quite apparently different at each stop. Yesterday’s luxuries are today’s basic human rights. I probably wouldn’t have to use up much of my remaining thorium to find a century that laughs at the idea of a school being a basic human right.
He also seems backwards on the outcomes of things like what you listed. Those things all raised people out of poverty and serfdom.
It’s interesting, though, to see someone as revered as Gandhi having to add epicycles to his beliefs after having seen the other side of it.
> It will grow into a full-scale industry and become the true infrastructure of all scientific and technological progress, a foundation that every other field stands on rather than a quiet corner of academia.
Sounds revolting. Everything being turned into the industry is soulless and uninspiring. I know a lot of people worship this future but I for one hate it. I for one don't see the point in creating this intellectual power where there will always, always be someone to abuse it simply because of our instinct to be greedy.
It will be the exact opposite: In a short period of time, many people will be able to prove or disprove a theorem. The mastery that used to require a decade of extensive study can now be had just by grabbing and applying an llm to the problem.
> I for one don't see the point in creating this intellectual power where there will always, always be someone to abuse it simply because of our instinct to be greedy.
Maybe your AI prevents the greedy AI from achieving their goals.
Yeah right. And do we really want to see another arms race? It's never a good thing for humanity.... It's clear from human interactions that the greedy and selfish usually have a leg up compared to those who have good intentions.
You sound pessimistic and uninspired. What alternative idea do you have besides, "it was better yesterday"? You accuse others of worshipping some dystopia but you just read like a misanthrope to me.
Duh? There is nothing left in the world to be excited about, it has been completely and totally strip mined for profit. We are sitting here in a post discussing the commoditization and industrialization of MATHEMATICS and you are confused that people are 'pessimistic'?
Speaking as a mathematician (or at least a former one) math has (at least from my perspective) become quite industrial and drab already. Most of the most interesting stuff has been solved already and a lot of it is just and endless race to generalize to stuff that interests in reality, very few. AI seems like the next stage in this process to me.
What are you talking about, that quote is quite literally from the article we are all discussing
> But it will not last. Mathematics is about to graduate. It will grow into a full-scale industry and become the true infrastructure of all scientific and technological progress
If your thesis is "that will not actually happen" then say that instead.
Sometimes, it really was "better yesterday". E.g., one might argue that people who grew up in the 90s in America had a much better qol than today, outside of the improvements in tech - which have been a double edged sword in terms of what they've done for human happiness.
It's okay to acknowledge things are worse than they used to be. It informs on the direction that we need to go to improve things. Not everything needs to be forwards just because some billionaires have willed it onto the rest of us.
Everything is awful and those billionaires ruined the world is just poisonous snark. i don't even see why you imagine saying that is clarifying or novel?
Encourage poeple to have a simpler life by using less technology, maybe? Stop inventing so much stuff and return to stronger, smaller communities? Use less AI? Take a few days away from the internet every week?
I believe in people, not tech. Tech past a certain point just makes things worse and always goes beyond a point of diminishing returns where its innovation becomes a mere arms race.
Not sure why people are stopping at 'AI can do advanced math!' and calling that the field is gonna transform due to LLMs specifically. Pretty much any meta-formulation of math gives you some initial rules and a goal. From natural deduction and sequent calculus to dependent type theory and whatever flavour of category theory you choose, at a sufficiently abstract level, you'll end up with some form of search problem. ATP folks foresaw machines doing automatic proofing for decades, but it seems that noone had enough incentive in pursuing it at the cost of suffering the tediousness of the encoding process. Now AI labs took the opportunity to do something impressive and have shown that it's possible to close the ergonomics gap. But the deeper achievement is the decades of ATP and proof-assistant work that make machine-generated proofs mechanically certifiable in the first place.
I am pretty sure in the next couple of years we'll see more evolved sledgehammers [0], maybe with LLM-like tech playing a role in encoding theorems, that will allow us to prove deeper than we can do manually, then help with the archeology and extraction of learnings from observing the 'trace' of certified proofs. So instead of explore -> understand -> solve, we'll get solve -> compress -> understand.
[0] e.g. https://isabelle.in.tum.de/website-Isabelle2025/dist/Isabell...
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.
Or that chess is over because stockfish can easily beat any human player. Or that warehouses don't need workers now that we have forklifts.
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.
The process of creating mathematical proofs from scratch is itself a rather high form of art, so I personally care even though I’m not a mathematician, because I enjoy the cultural effects within science. A world without future inspiring stories like Yitang Zhang seems rather dull and gray in my view. And by the way, Stockfish did kill correspondence chess, the form of chess most similar to academic research, chess that was unproctored and untimed.
How big are mathematics? Is it as big as the universe?
I think likely to be infinite, per Gödel's incompleteness theorems. Given a corpus of maths called A we can always find new unprovable axioms under A, giving us a new corpus. From there we can prove new theorems.
There may be a finite point at which we've proven and codified everything but the most inane meta-meta-meta-maths though.
That is a very interesting perspective. What is the purpose of that corpus. Are all theorems or axioms useful?
That's now how it works. You generally can't know if a statement is provable/unprovable under A. In most cases, there's nothing to identify a new corpus.
No, it’s not. The telescopes are not searching the sky and logging down the results by themselves.
https://www.space.com/google-cloud-ai-tool-asteroid-telescop...
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...
Can we ban glib just-so comments?
This piece reminded me, of all things, of Gandhi's essay "Hind Swaraj." He was pretty anti-technological-driven change.
He was anti: - Machinery replacing handicraft (skill disappeared and poverty followed) - Labor-saving machines replacing human workers (workers became expendable) - Doctors replacing consequences (people lost self-control) - Railways replacing constraint and slowness (harm spread faster)
But he loved the sewing machine.
Gandhi’s test for whether to accept tech-driven change was whether it satisfied primary needs. Interpretation of those needs was certainly not universal. As he wrote: "...it is not the primary need of man to traverse distances with the rapidity of a motor car. The needle on the contrary happens to be an essential thing in life, a primary need.”
That's the airplane in this post. Excitement or fear of the AI airplane is either judged as helping mathematicians (sewing machine) or doing something not quite right (the above machinery/doctor/railway)...
Gandhi’s argument seems flawed. It’s arbitrary to decide the needle is a primary need because it requires delineation of need vs. want. If we took a time machine back every 100 years, that delineation would be quite apparently different at each stop. Yesterday’s luxuries are today’s basic human rights. I probably wouldn’t have to use up much of my remaining thorium to find a century that laughs at the idea of a school being a basic human right.
He also seems backwards on the outcomes of things like what you listed. Those things all raised people out of poverty and serfdom.
It’s interesting, though, to see someone as revered as Gandhi having to add epicycles to his beliefs after having seen the other side of it.
This is probably the inescapable conclusion that most in the current panic-filled era of Math research discourse will come to, one way or another.
> It will grow into a full-scale industry and become the true infrastructure of all scientific and technological progress, a foundation that every other field stands on rather than a quiet corner of academia.
Sounds revolting. Everything being turned into the industry is soulless and uninspiring. I know a lot of people worship this future but I for one hate it. I for one don't see the point in creating this intellectual power where there will always, always be someone to abuse it simply because of our instinct to be greedy.
It will be the exact opposite: In a short period of time, many people will be able to prove or disprove a theorem. The mastery that used to require a decade of extensive study can now be had just by grabbing and applying an llm to the problem.
> I for one don't see the point in creating this intellectual power where there will always, always be someone to abuse it simply because of our instinct to be greedy.
Maybe your AI prevents the greedy AI from achieving their goals.
"Good guy with an AI"
Yeah right. And do we really want to see another arms race? It's never a good thing for humanity.... It's clear from human interactions that the greedy and selfish usually have a leg up compared to those who have good intentions.
[delayed]
You sound pessimistic and uninspired. What alternative idea do you have besides, "it was better yesterday"? You accuse others of worshipping some dystopia but you just read like a misanthrope to me.
> You sound pessimistic
Duh? There is nothing left in the world to be excited about, it has been completely and totally strip mined for profit. We are sitting here in a post discussing the commoditization and industrialization of MATHEMATICS and you are confused that people are 'pessimistic'?
What were we excited about before? The unknown? There is still plenty of that. Now is there is this machine that lies between us and the unknown.
But nothing you said was true? So aren't you just sad and letting bad ideas color your worldview?
Speaking as a mathematician (or at least a former one) math has (at least from my perspective) become quite industrial and drab already. Most of the most interesting stuff has been solved already and a lot of it is just and endless race to generalize to stuff that interests in reality, very few. AI seems like the next stage in this process to me.
What are you talking about, that quote is quite literally from the article we are all discussing
> But it will not last. Mathematics is about to graduate. It will grow into a full-scale industry and become the true infrastructure of all scientific and technological progress
If your thesis is "that will not actually happen" then say that instead.
Sometimes, it really was "better yesterday". E.g., one might argue that people who grew up in the 90s in America had a much better qol than today, outside of the improvements in tech - which have been a double edged sword in terms of what they've done for human happiness.
It's okay to acknowledge things are worse than they used to be. It informs on the direction that we need to go to improve things. Not everything needs to be forwards just because some billionaires have willed it onto the rest of us.
Everything is awful and those billionaires ruined the world is just poisonous snark. i don't even see why you imagine saying that is clarifying or novel?
The first step is admission
Encourage poeple to have a simpler life by using less technology, maybe? Stop inventing so much stuff and return to stronger, smaller communities? Use less AI? Take a few days away from the internet every week?
I believe in people, not tech. Tech past a certain point just makes things worse and always goes beyond a point of diminishing returns where its innovation becomes a mere arms race.
Encourage poeple to have a simpler life by using less technology, maybe? Stop inventing so much stuff and return to stronger, smaller communities?
Other sites beckon.