Greg Egan's description of how mathematics evolves into "truth mining" in his novel Diaspora is seeming more and more prescient. It essentially describes what mathematics would look like after formalization records all theorems discovered so far in a huge, collective database and proof assistants can instantly work out the details of a given proof. What remains of mathematics? According to Egan, visualization, intuition, and insight.
One of the most fruitful approaches in mathematics is to flip back and forth between geometric and algebraic views of a problem. I think this works so well because these are actually handled by two different parts of the brain on a physical level; spatial reasoning is separate from language processing. Cytoarchitecture shows these regions have different "textures;" the local details of the way neurons are wired together are simply different in these different regions of the brain, in the same way a CNN and a transformer have different topologies. Thus, by flipping problems from geometry to algebra and vice versa, we're able to bring an entirely different cognitive style to bear on a problem. For example, the proof of Monge's Theorem by moving to 3D and visualizing not three circles, but three spheres sitting on a table with a book on top of them and then pointing out that the intersection of two planes is a line. What is pages of unintuitive symbol pushing turns into something a child can understand. Going the other way, things like the angle addition formulas or the quadratic formula, which are quite hard to prove geometrically, become quite simple if you use a little algebra.
Current-gen LLMs are still relatively weak at visual reasoning; see the Vision Language Models are Blind paper, for example, or the ARC-AGI benchmark. So that's one way humans can stay ahead of the agents, at least for now.
show comments
credit_guy
People think mathematics is about proving theorems.
I think that's just an accident of history.
When we write software, we very seldom write proofs that our algorithms are correct. We just write tests, and we also run the algorithms and when they fail we know we have a bug and then we proceed to debug, fix, and add new tests (if we are disciplined, but most of us are). In time, by usage and testing, we gain confidence that our battle tested software is correct, mostly. And we tell people that we will never be 100% confident that any software is bug free. But that's a slight lie: if we wanted such confidence, we would start using provers, and create bug-free software. That possibility exists, but it's just extraordinarily expensive.
Well, in math that's the only possibility, and we use it. And it is indeed extraordinarily expensive, but it's also the cheapest among the alternatives. The alternatives are 2: be rigorous and do these proofs, or be sloppy and allow bugs to creep in, and allow an entire school of math to collapse like the Italian school of algebraic geometry [1].
There is one more alternative. If a particular math theorem has some applicability, then you write a program and use it in real life. In time you eliminate the bugs as much as you can, and you get to the steady state of "virtually bug free". At that point you don't have a solid proof that the theorem is correct, but in general you don't really care. Because you feel that a formal proof is just a thing one would pursue for getting academic satisfaction only.
+-- 2mo before by sdfrew
| 4 points / 1 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=47862472
|
+-- 2mo before by fuglede_
| 3 points / 1 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=47891494
|
+-- 2mo before by mathgenius
| 2 points / 0 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=47909751
|
+-- 2mo before by delis-thumbs-7e
| 15 points / 4 comments
| David Bessis on AI destroying mathematics
| https://news.ycombinator.com/item?id=47985962
|
+-- 1mo before by magoghm
| 4 points / 0 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=48084737
|
+-- 1mo before by cubefox
| 2 points / 0 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=48089716
|
+-- 1mo before by cubefox
| 5 points / 0 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=48152469
|
+-- 1mo before by tmp10423288442
| 4 points / 1 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=48214866
|
`-- this submission by varjag
58 points / 7 comments
The Fall of the Theorem Economy
https://news.ycombinator.com/item?id=48758048
stackbutterflow
Tangential but this article got me thinking.
Are we going to see less publicly shared science? With private actors or governments restricting access to AI resources to a few scientists and keeping new knowledge to themselves.
Advancing science in the open was the best strategy when there was real advantage to share the load with every brain on the planet willing to give a try at science, but if a computer can match or surpass the collective output of the entire human scientific community the equation will change.
It's a sad outlook.
show comments
mojosmojo
Incredibly thoughtful. This essay gives that very rare sense of being well reasoned, gods at forest and trees, and sitting atop a shit ton of domain expertise.
This kills me, it is correct, but misses the forest for the trees. Yes, mathematics is a discipline of understanding, but an insular one. The entire field is about trying to understand, but the discipline does not try to be understood. No, that is "your job, not theirs" and that is why this discipline is struggling, struggling in a culture that can barely communicate without emotional morons destroying any constructive communications.
show comments
whack
The core thesis seems to be that the "real value" is not in producing/proving theorems, but in understanding them. AI might be good at producing and proving theorems, but it fails utterly at getting humans to understand them. Even worse, humans have no interest in working on theorems that have already been proven, so we end up with theorems that will never be understood by humans.
I can understand why this is a major concern for mathematicians. They got into their field because they love the beauty of mathematics, and the intellectual satisfaction of understanding non-obvious insights. But to put it crudely, this sounds like a you problem. As someone who isn't a mathematician, the main value I get out of math is its practical applications in science and technology. And their practical applications in human life. I have zero understanding of the math behind cryptography, but I still deeply appreciate the practical value they have provided humanity.
If AI systems start churning out accurate theorem-proofs, and we are able to use those theorems to build things that improve human quality of life, it doesn't bother me one bit that those theorems have not been understood by humans. If this offends your aesthetics, you are certainly entitled to your opinion and your preferences, but that does not make it a societal problem
show comments
rbanffy
> to come up with a conceptual framework where it became easy to express
Feels a lot like building software from bottom - once you get the building blocks defined right, the action, or the program, are trivial to express. When doing it from the top-down, you write the program using the building blocks you haven't defined yet, and you might end up with overly specific building blocks, needing other blocks for expressing different behaviors.
When you do the bottom-up building blocks right, new behavior is easy to express with them. Essentially, you are building up the language to reach the problem. Or making a DSL, whatever definition you like best.
show comments
a1o
From reading this, it looks like the projected future is mathematicians working more applied to a domain, and the basic research in the academia being severely impacted by the AI companies - who have the money to hire the senior mathematicians from the academia. I guess if some of the biggest universities could come up with their own AI powered programs there could be something to “answer” in a more accessible knowledge, but I don’t see how to properly keep the students motivated to ensure the field keeps producing new people.
j7ake
Does the the (,1) conjecture paper in annnals of Math say 7 years between submission and acceptance? Insane
show comments
jdw64
Someday, there might be mathematics designed for AI. Mathematics that only a tiny fraction of humans can understand, but a different kind of mathematics might emerge. I wonder if we would still call it mathematics.
What would happen if a non-human layer of mathematics emerged on top of human mathematics? In this article, the distinction between Mathlib and Mathslop might be a precursor to that.
If models advance enough in the future, and new definitions, compressions, and representational forms that are convenient for AI-to-AI communication emerge, what would happen then? Would mathematics split into Human-facing and Machine-facing branches?
show comments
codemog
> Some prophesy that mathematics will eventually resemble Chess, a sport that a few eccentrics practice with passion and the general public can safely ignore.
How is it not already this? Jon von Neumann was already calling most math this many decades ago. Pull up any random arxiv math paper and it’s abstract nonsense with no applications to the real world.
guelo
When math is so divorced from science and engineering that there's no conceivable way that it will ever be applied in the real world then it is just a complex puzzle game that a tiny group of people play. It doesn't really matter much. If the 200,000 line Mathslop proof has no real world application and it doesn't help the puzzle solvers then it is double useless.
show comments
Staross
I thought it was very interesting, but maybe also incredibly naive politically ? it's like he's re-discovering alienation under capitalism.
A wood-worker could do the same argument, there's the "official" wood-working word of perfect joinery and beautifully finished tables one can buy, but behind it there's the "secret" messy human element, the art, the craft, the mistakes and hard-ships, the elevation of human skills and imagination, the creation of whole new types of wood-working inventions and techniques, the perpetuation of millenia-old traditions, the teaching, the joy of selling to a happy customer, etc.
But now comes techo-capitalism, division of labor, you cut that piece a that piece over and over, you operate that machine, you won't even see the finished table, fuck your human element, we want that profit !
show comments
daxfohl
To be devil's advocate, two things may offer a glimmer of hope:
First, math, generally, is useless. I mean, yes there are of course practical uses of basic thru undergrad-level math, and some beyond that. But for many mathematicians, the sum result of their entire career may lead to exactly zero results that have any real-world value. The entire field they work in may have meaning only to the handful of other individuals on the planet that also work in that field. But to those handful of people, the meaning defines their lives. From a socio-economic perspective, those departments should have been defunded a century ago. Yet they continue. Why? Because it scratches an itch. Not just for those individuals in the field, but also for us as a species. To stop exploring, to eliminate the search for pots of gold that may be buried in some odd corner of sphere packing, or coloring theorems, or Garside categories, and to put a boundary on the limits of our understanding, just because they aren't immediately applicable, is an idea that most humans would not be willing to sacrifice, even if it reduced their tax burden a couple cents. If it was going to happen, it'd have happened already.
The second is, even with AI, it's not free. As the software industry is discovering, far from it. So, given that, who is going to decide what theorems to research and how much it's worth? Congress? Of course not. AI itself? In theory that sounds plausible, but that falls victim to thing 1 above: most math is useless, so AI itself has no value metric it can assign to things, and besides which, without the human element, once the initial curiosity has subsided, there'd be no reason to continue any funding for AI to do it. So no, the only possible owners of this is going to be mathematicians themselves, the ones who care about the field and deeply understand the kwah of their vision.
Combining these, there's a future where, humanistically, "nothing changes". The method changes, the efficiency changes, the scope changes, but the work itself: publishing proofs, remains the domain of professional mathematicians. AI will enable them to be dramatically more daring and broad in their investigations and scope, and will likely write the entirety of the proof. However it will remain the work of the mathematicians to determine, what areas are worth spending limited AI resources on to investigate further, how far to go down rabbit holes, how to prioritize potential connections, and what the ultimate meaning of the findings is. So rather than being an end of mathematics, it could be a dawn of something far greater than anything we've ever seen before.
cubefox
This might be the most interesting essay on the nature of mathematics I have ever read.
asdfsa32
Is being pompous and on the nose part of being in mathematics?
"I was in Switzerland", "I was invited to a talk", "I started a machine learning company", look at me bro.
show comments
khalic
I see the AI panic has reached mathematics…
throwaway81523
I've only started reading it but it looks very good. I'll finish it tomorrow or so.
Greg Egan's description of how mathematics evolves into "truth mining" in his novel Diaspora is seeming more and more prescient. It essentially describes what mathematics would look like after formalization records all theorems discovered so far in a huge, collective database and proof assistants can instantly work out the details of a given proof. What remains of mathematics? According to Egan, visualization, intuition, and insight.
One of the most fruitful approaches in mathematics is to flip back and forth between geometric and algebraic views of a problem. I think this works so well because these are actually handled by two different parts of the brain on a physical level; spatial reasoning is separate from language processing. Cytoarchitecture shows these regions have different "textures;" the local details of the way neurons are wired together are simply different in these different regions of the brain, in the same way a CNN and a transformer have different topologies. Thus, by flipping problems from geometry to algebra and vice versa, we're able to bring an entirely different cognitive style to bear on a problem. For example, the proof of Monge's Theorem by moving to 3D and visualizing not three circles, but three spheres sitting on a table with a book on top of them and then pointing out that the intersection of two planes is a line. What is pages of unintuitive symbol pushing turns into something a child can understand. Going the other way, things like the angle addition formulas or the quadratic formula, which are quite hard to prove geometrically, become quite simple if you use a little algebra.
Current-gen LLMs are still relatively weak at visual reasoning; see the Vision Language Models are Blind paper, for example, or the ARC-AGI benchmark. So that's one way humans can stay ahead of the agents, at least for now.
People think mathematics is about proving theorems.
I think that's just an accident of history.
When we write software, we very seldom write proofs that our algorithms are correct. We just write tests, and we also run the algorithms and when they fail we know we have a bug and then we proceed to debug, fix, and add new tests (if we are disciplined, but most of us are). In time, by usage and testing, we gain confidence that our battle tested software is correct, mostly. And we tell people that we will never be 100% confident that any software is bug free. But that's a slight lie: if we wanted such confidence, we would start using provers, and create bug-free software. That possibility exists, but it's just extraordinarily expensive.
Well, in math that's the only possibility, and we use it. And it is indeed extraordinarily expensive, but it's also the cheapest among the alternatives. The alternatives are 2: be rigorous and do these proofs, or be sloppy and allow bugs to creep in, and allow an entire school of math to collapse like the Italian school of algebraic geometry [1].
There is one more alternative. If a particular math theorem has some applicability, then you write a program and use it in real life. In time you eliminate the bugs as much as you can, and you get to the steady state of "virtually bug free". At that point you don't have a solid proof that the theorem is correct, but in general you don't really care. Because you feel that a formal proof is just a thing one would pursue for getting academic satisfaction only.
[1] https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge...
Some previous submissions
HN history
Tangential but this article got me thinking.
Are we going to see less publicly shared science? With private actors or governments restricting access to AI resources to a few scientists and keeping new knowledge to themselves.
Advancing science in the open was the best strategy when there was real advantage to share the load with every brain on the planet willing to give a try at science, but if a computer can match or surpass the collective output of the entire human scientific community the equation will change.
It's a sad outlook.
Incredibly thoughtful. This essay gives that very rare sense of being well reasoned, gods at forest and trees, and sitting atop a shit ton of domain expertise.
I built a toy autonomous math research project: https://paulklemstine.github.io/Lean/
This kills me, it is correct, but misses the forest for the trees. Yes, mathematics is a discipline of understanding, but an insular one. The entire field is about trying to understand, but the discipline does not try to be understood. No, that is "your job, not theirs" and that is why this discipline is struggling, struggling in a culture that can barely communicate without emotional morons destroying any constructive communications.
The core thesis seems to be that the "real value" is not in producing/proving theorems, but in understanding them. AI might be good at producing and proving theorems, but it fails utterly at getting humans to understand them. Even worse, humans have no interest in working on theorems that have already been proven, so we end up with theorems that will never be understood by humans.
I can understand why this is a major concern for mathematicians. They got into their field because they love the beauty of mathematics, and the intellectual satisfaction of understanding non-obvious insights. But to put it crudely, this sounds like a you problem. As someone who isn't a mathematician, the main value I get out of math is its practical applications in science and technology. And their practical applications in human life. I have zero understanding of the math behind cryptography, but I still deeply appreciate the practical value they have provided humanity.
If AI systems start churning out accurate theorem-proofs, and we are able to use those theorems to build things that improve human quality of life, it doesn't bother me one bit that those theorems have not been understood by humans. If this offends your aesthetics, you are certainly entitled to your opinion and your preferences, but that does not make it a societal problem
> to come up with a conceptual framework where it became easy to express
Feels a lot like building software from bottom - once you get the building blocks defined right, the action, or the program, are trivial to express. When doing it from the top-down, you write the program using the building blocks you haven't defined yet, and you might end up with overly specific building blocks, needing other blocks for expressing different behaviors.
When you do the bottom-up building blocks right, new behavior is easy to express with them. Essentially, you are building up the language to reach the problem. Or making a DSL, whatever definition you like best.
From reading this, it looks like the projected future is mathematicians working more applied to a domain, and the basic research in the academia being severely impacted by the AI companies - who have the money to hire the senior mathematicians from the academia. I guess if some of the biggest universities could come up with their own AI powered programs there could be something to “answer” in a more accessible knowledge, but I don’t see how to properly keep the students motivated to ensure the field keeps producing new people.
Does the the (,1) conjecture paper in annnals of Math say 7 years between submission and acceptance? Insane
Someday, there might be mathematics designed for AI. Mathematics that only a tiny fraction of humans can understand, but a different kind of mathematics might emerge. I wonder if we would still call it mathematics.
What would happen if a non-human layer of mathematics emerged on top of human mathematics? In this article, the distinction between Mathlib and Mathslop might be a precursor to that.
If models advance enough in the future, and new definitions, compressions, and representational forms that are convenient for AI-to-AI communication emerge, what would happen then? Would mathematics split into Human-facing and Machine-facing branches?
> Some prophesy that mathematics will eventually resemble Chess, a sport that a few eccentrics practice with passion and the general public can safely ignore.
How is it not already this? Jon von Neumann was already calling most math this many decades ago. Pull up any random arxiv math paper and it’s abstract nonsense with no applications to the real world.
When math is so divorced from science and engineering that there's no conceivable way that it will ever be applied in the real world then it is just a complex puzzle game that a tiny group of people play. It doesn't really matter much. If the 200,000 line Mathslop proof has no real world application and it doesn't help the puzzle solvers then it is double useless.
I thought it was very interesting, but maybe also incredibly naive politically ? it's like he's re-discovering alienation under capitalism.
A wood-worker could do the same argument, there's the "official" wood-working word of perfect joinery and beautifully finished tables one can buy, but behind it there's the "secret" messy human element, the art, the craft, the mistakes and hard-ships, the elevation of human skills and imagination, the creation of whole new types of wood-working inventions and techniques, the perpetuation of millenia-old traditions, the teaching, the joy of selling to a happy customer, etc.
But now comes techo-capitalism, division of labor, you cut that piece a that piece over and over, you operate that machine, you won't even see the finished table, fuck your human element, we want that profit !
To be devil's advocate, two things may offer a glimmer of hope:
First, math, generally, is useless. I mean, yes there are of course practical uses of basic thru undergrad-level math, and some beyond that. But for many mathematicians, the sum result of their entire career may lead to exactly zero results that have any real-world value. The entire field they work in may have meaning only to the handful of other individuals on the planet that also work in that field. But to those handful of people, the meaning defines their lives. From a socio-economic perspective, those departments should have been defunded a century ago. Yet they continue. Why? Because it scratches an itch. Not just for those individuals in the field, but also for us as a species. To stop exploring, to eliminate the search for pots of gold that may be buried in some odd corner of sphere packing, or coloring theorems, or Garside categories, and to put a boundary on the limits of our understanding, just because they aren't immediately applicable, is an idea that most humans would not be willing to sacrifice, even if it reduced their tax burden a couple cents. If it was going to happen, it'd have happened already.
The second is, even with AI, it's not free. As the software industry is discovering, far from it. So, given that, who is going to decide what theorems to research and how much it's worth? Congress? Of course not. AI itself? In theory that sounds plausible, but that falls victim to thing 1 above: most math is useless, so AI itself has no value metric it can assign to things, and besides which, without the human element, once the initial curiosity has subsided, there'd be no reason to continue any funding for AI to do it. So no, the only possible owners of this is going to be mathematicians themselves, the ones who care about the field and deeply understand the kwah of their vision.
Combining these, there's a future where, humanistically, "nothing changes". The method changes, the efficiency changes, the scope changes, but the work itself: publishing proofs, remains the domain of professional mathematicians. AI will enable them to be dramatically more daring and broad in their investigations and scope, and will likely write the entirety of the proof. However it will remain the work of the mathematicians to determine, what areas are worth spending limited AI resources on to investigate further, how far to go down rabbit holes, how to prioritize potential connections, and what the ultimate meaning of the findings is. So rather than being an end of mathematics, it could be a dawn of something far greater than anything we've ever seen before.
This might be the most interesting essay on the nature of mathematics I have ever read.
Is being pompous and on the nose part of being in mathematics?
"I was in Switzerland", "I was invited to a talk", "I started a machine learning company", look at me bro.
I see the AI panic has reached mathematics…
I've only started reading it but it looks very good. I'll finish it tomorrow or so.