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.
Spot on! Love Diaspora. This is honestly such a gem of a comment. To some extent, if the AI ever gets "so far ahead" of humans, the most productive aspect will be the frontier visible to humans. We're focused on translating mathematics to lean at the moment, but it'll be as important to translate it to humanese - to the human language of structure, number, geometry. I also completely agree with LLMs being essentially blind to visual reasoning. They really struggle reasoning with Floer Heegard diagrams for example.
i got so inspired by reading diaspora this year that i instantly started working on some polisware. cipherclerk operational: https://github.com/emberian/dregg
topical to the conversation, it is fully formally verified in lean (with some UC security reductions done in isabelle). also did this in HOL4 inspired by some work i did with ramana kumar in 2016, on reflective self-verifying self-modifying systems: https://github.com/emberian/svenvs
I took a look at dregg, I like the idea for an README-LLMS.txt. It seems like a good way to not only communicate to other LLM users (which we should be thinking more of doing effectively) but also I can imagine it’s helpful for your own new sessions with an LLM to arm them with proper context.
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.
Your example of the Italian school is well taken, although most of their results were later proven to be correct in the right setting. Severi's example is particularly egregious and I think a major reason this became a thing is Severi's refusal to course-correct and accept that some of the results were not correct. It has echoes of Mochizuki, and I fear, once you dig deeper, some issues around the initial declaration of "We've proven the Classification of Finite Simple Groups". There were many genuine gaps, and a lot of lore taken for granted. The sociology around how this happened is interesting - rushing to announce that it was done was the major mistake, it took away almost all incentive to actually write up the proofs and take them through proper peer-review. Genuine mathematical work was falsely reduced to "write up".
This is a bit reductive about what "proof" actually means in mathematics. Even in math, the kind of formal proofs that tools like Coq can automatically verify are an extreme, and lots of accepted and practiced math is not doing that. Proofs are often more abstract and even occasionally hand-wavy (for example not proving "obvious" statements or minor lemmas).
Mathematicians also occasionally build on top of unproven foundations (e.g. all popular asymmetric encryption schemes are built on top the assumption that certain problems such as integer factoring are hard, for which there is no formal proof), or at least explore both possibilities for statements with unknown truth value (e.g. you can find lots of work that explores the consequences of P = NP and/or P != NP).
However, there is a major separation between math and programs that I think mostly invalidates your proposal - most math we're talking about here is simply not applicable directly to the real world in any way. It's only studied for the interest of mathematicians. There is no real world consequence for Fermat's last theorem, for example - it was just a really interesting to prove theorem. In directly applied math, such as engineering, it is in fact much more common to work with unproven but well tested conjectures.
> In directly applied math, such as engineering, it is in fact much more common to work with unproven but well tested conjectures.
What specific areas were you thinking off? I don't recall, e.g., in numerics that things were often just unproven/conjectures, but might be subject matter specific.
Well, it's not exactly engineering, but physics often uses quite informal math. For a pretty modern example, the Dirac delta "function" was used long before it was formally described; and I have heard it said that even today String theory uses some math that is not fully formalized - though I can't say I know what specifically, so I may be wrong. Newton expressed calculus in terms of inifinitesimals (the dx notation was simply an infinitesimal delta x, not merely notation for derivation), which were not not formalized until much later, after they had already fallen out of favor and had been replaced in formal math by the delta-epsilon limits-based constructions.
Edit: one better example from modern physics - the path integral formulation, used in both string theory and other areas of QM/QFT, is not fully formalized and formally proven to work. Also, a more concrete example of a widely used but actually still unproven conjecture in string theory is the famous AdS/CFT correspondence.
It's interesting that mathematics, which is mostly recreational (I received profound disdain at the math department for asking about applications!) has such rigorous standards, but software, which entire civilizations now run on, does not.
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.
The intelligence is only one part of the story. People need to actually go out there and do experiments. Science is not only theory, but also experimental. The best science happens when experiments show that a previously held assumption was not true. Eg the Michaelson Morley experiment where the assumption of ether was disproved. While AI is an incredibly powerful tool, it does not replace the act of observation. Thus Im sure we will still have scientists in the future and some degree of open science. There are experiments out there that by nature of their complexity need massive public coordination (CERN for instance) which in turn benefits from openness.
What is going to suck though is the ladder for juniors. We dont start out by working on big ticket problems, but usually early career researchers solve really tiny problems in a cheap way. The lowest bar for a cash strapped PhD student would be to contribute to some new theory in some way even if the student doesnt have access to equipment.
Ah I see your point, I took the word science to mean bio, physics, chemistry, etc. IMO mathematics is a different discipline and not one Id consider a science, rather I see it as the language with which we express science.
If AI is somehow able to prove everything wouldn't it bypass Godel's incompleteness theorems?
It's not even just science. Anyone producing anything digital is now heavily incentivized to keep their wares away from the public internet, in a way we've not seen before. Drop any sample of your unique production online, and the AIs will obsolete you in days. That is a massive loss for people looking for inspiration and guidance.
> to share the load with every brain on the planet willing to give a try at science
This is what a lot of scientists love to tell themself or talk about in celebratory speeches.
The truth is: a lot of science is kept behind journal paywalls, so that only "officially approved" (in the sense of: working at a university or an governmental research institute) scientists can easily access it.
You know how I read new papers back in 1994? By going to the library, finding one in bi-annual publication list and requesting it through the University system. And it better be necessary because the uni had to pay both the catalogue and each reprint of an article. The access is most certainly easier today.
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.
+-- 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
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
They got into their field because they love the beauty of mathematics… As someone who isn't a mathematician, the main value I get out of math is its practical applications in science and technology
I have some sad news for you. 99% of the work mathematicians do has no immediate application, nor even an obvious path toward application in the near future. You mentioned cryptography, so for an example consider number theory: no apparent practical applications, going back thousands of years to the time of Euclid and earlier.
It’s been religion, philosophy, and recreation that have provided the motivations to study mathematics all these years, not applications. Applications have almost always followed long after the development of the pure mathematical theory. For number theory, that was the development of cryptography during WW2, millennia after the ancients laid those foundations.
Most unfortunately, it’s the truth value and the understanding which drive applications of mathematics, not the proof work itself. If the AI revolution decapitates the institution of mathematics which produces the understanding, and is unable to replace it, then the applications will cease as well.
Then you have to make sure that the AIs understand the theorems (sort of build a "world" for that - otherwise how'd there be confidence in the use of said theorems?
If cryptography didn't exist but the maths did, how'd you use it?
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.
> 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.
Well, it depends. Sometimes in math you do a lot of chipping away at a problem, and eventually a bigger result falls after all the right foundations are built. That seems to describe bottom-up building.
On the other hand when a new high-level concept becomes clear and seems to emerge like a revelation, and people start thinking in terms of those new definitions, it seems that a hundred pages worth of smaller results can fall out of it almost effortlessly. This way of describing it is more top-down.
I don't know that there's an exact parallel with software. Math keeps feeding into itself in a way that software dreams about with our ambitions of code reuse. The old Object Oriented dreams of perfectly encapsulated classes and abstractions partially worked out, but not to the degree that was envisioned.
The current situation with package managers doesn't look like a tower that keeps growing higher and higher levels of abstractions. It looks like a tower where each person wants to place one tiny brick that they call left-pad, and next year we will rebuild the lower levels instead of going higher. So the top-down and bottom-up building that we do is different. We keep rebuilding the bottom, and we don't very much like when the tower of abstractions get too tall and hard to reason about.
Well, it depends. Sometimes in math you do a lot of chipping away at a problem, and eventually a bigger result falls after all the right foundations are built. That seems to describe bottom-up building.
On the other hand when a new high-level concept becomes clear and seems to emerge like a revelation, and people start thinking in terms of those new definitions, it seems that a hundred pages worth of smaller results can fall out of it almost effortlessly. This way of describing it is more top-down.
I don't know that there's an exact parallel with software. Math keeps feeding into itself in a way that software dreams about with our ambitions of code reuse. The old Object Oriented dreams of perfectly encapsulated classes and abstractions partially worked out, but not to the degree that was envisioned.
The current situation with package managers doesn't look like a tower that keeps growing higher and higher levels of abstractions. It looks like a tower where each person wants to place one tiny brick that they call left-pad, and next year we will rebuild the lower levels instead of going higher. So the top-down and bottom-up building that we do is different. We keep rebuilding the bottom, and we don't very much like when the tower of abstractions get too tall and hard to maintain.
These stories are common in math, e.g. these recently happened to me, a lowly mathematician:
1) Two and a half years with no reply from a journal (not even to emails I sent that I'd like to retract the paper so I could send it somewhere else). Then suddenly they tell me the paper is accepted.
2) One year with no reply. Then, my "anxious" collaborator sends them countless emails and gets redirected from person to person and finally an editor tells us that they decided almost immediately to reject our paper but they didn't tell us because "they hate giving bad news".
These were not top journals like Annals, but decent, prestigious ones, from whom you'd expect some professionalism.
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?
Science is not about results, it is about the transmission of knowledge. So long as those AI-"sciences" are just inside AI, they are "engineering", not science.
I am not dismissing engineering (it moves the world we live in), just trying to clarify what science is.
Applied fluid dynamics works like that: noone has ever really "verified" that the finite-element method applied to some specific model does converge
Agree, but more specifically Math is clearly about a human understanding structure of things. Math is basically for humans. It's one of the main reasons understandable proof is so important.
That’s a strange delineation. Engineering is essentially about designing a thing, asking whether that thing really does satisfy the desired criteria, and then iterating when it does not. Mathematical models of the world are tremendously useful to this practice—engineers don’t need to guess about many aspect of the real world: they have physics. What they want, more than anything else, is strong evidence that a property holds. Internal validity (proof) and external validity (experiment) are the best evidence that you can get—why would you throw one of those approaches away?
So what I’m most curious about is this: if there are axioms and proofs so enormous that a human could never prove them in a lifetime, but a machine can, does that make it engineering? That’s the point I’m really wondering about.
I mean, what if a human could follow every single step of the process in principle, but the sheer volume is so vast that a human can never see the whole thing—would that be engineering?
But I don’t think of that as engineering. In the future, maybe it will be called an Oracle
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.
Eh? I thought this was the main thrust of the argument: Mathematics has in fact always prized conceptual advancement and understanding over proof, despite presenting itself internally and externally as rewarding the latter. The author calls what he’s proposing “rebranding a plurimillenial project”.
The proposal needs to be larger, to education itself in all subjects. We are manufacturing too many specialist parrots without critical analysis. We need to teach how to discuss controversy and manage disagreements, and then we can start making progress.
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.
Right; this is my viewpoint too. All the "pure mathematicians" have a bleak future where AI can do all the puzzle solving better and faster. They existed in their own world elevating "theorem proving within a formal system" as the central aspect of "proper" mathematics and everything else as ancillary.
It always felt wrong to me that while the scientific method iterated starting with the "real world" viz. Observe, Measure, Hypothesize (includes modeling with mathematics), Test and Refine; pure mathematicians lost themselves in the formalization of hypothesizing/modeling and thus lost touch with mapping it to reality. The AI revolution is now showing them up.
Yes. Though even philosophy, which doesn't have the "real world" iteration that science does, arguably doesn't have the problems of pure mathematics.
Pure mathematicians create ever more abstractions and get lost in solving puzzles on how these abstractions logically relate to each other. But since these abstractions don't have any relevance outside of pure mathematics, it's an entirely self-referential game, like chess. Except that nobody confuses being a professional chess player with being a noble researcher.
Even in philosophy, at least analytic philosophy, that issue of getting lost in your own abstractions doesn't really exist. Because analytic philosophy doesn't analyze its own concepts, it analyzes the concepts that already exist in natural language. Like truth, knowledge, probability, causation, belief, desire, consciousness, rationality and so on. These concepts come from outside of philosophy, and they have independent relevance for non-philosophers.
In contrast, pure mathematics seems to be the part of mathematics that only has relevance to pure mathematicians. Similar to how a game like chess has only relevance to chess players, not to anything entirely unrelated to chess. But again, people who are into mastering some game or sport are fully aware that what they are trying to master is a self-contained game, or a sport, not something that increases the amount of human knowledge beyond that.
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 !
You start with instincts that are more easily ascribed to ethically-neutral or ethically-positive reasoning, and then turn them into a spurious criticism of capitalism. Case in point: in the USSR, the means of producing chairs were 100% state-controlled and not motivated by profit, but the country operated soulless production lines too.
The motivation behind all this is less "haha I want profit" and more "billions of people need chairs, approximately none of them care about the craftsmanship, so it's in our best interest to make furniture in the most resource- and labor-efficient way possible". Even if the state subsidizes the production of handcrafted chairs, the population is the poorer for it on a resource allocation basis, because we now need a million artisanal chair-makers instead of a bunch of factories.
I don't think you have it right- the analogy to woodworking and craftsmanship is a category error and probably misses the broad thrust of the essay.
The goal of a woodworker or craftsman is the production of a finished good. He's arguing that, although it's been convenient to position a mathematician as a
"theorem-producer", that's never really been the aim of mathematics, and that the actual products of mathematics are some kind of "mental software"-
see his references to neuroplasticity. Basically, he's saying that the goal of mathematics is to create abstract structures that allow humans to reason about increasingly complex concepts, and that the "mathematician as theorem producer" is more like a convenient fiction that mathematicians have allowed to persist for too long, and now threatens to endanger the whole practice of mathematics.
Being invited to conference talks around the world is a completely normal part of being an active researcher in almost any academic field, so it doesn't register as pompous to other academics.
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.
LLMs sure, but AlphaZero had no visual cortex yet can smash Magnus Carlsen easily.
I think that we're not that far away from AI that can be superhuman at all facets of theorem proving.
I think that we're far away from an AI that can create good abstractions and construct a theory to prove theorems.
Spot on! Love Diaspora. This is honestly such a gem of a comment. To some extent, if the AI ever gets "so far ahead" of humans, the most productive aspect will be the frontier visible to humans. We're focused on translating mathematics to lean at the moment, but it'll be as important to translate it to humanese - to the human language of structure, number, geometry. I also completely agree with LLMs being essentially blind to visual reasoning. They really struggle reasoning with Floer Heegard diagrams for example.
i got so inspired by reading diaspora this year that i instantly started working on some polisware. cipherclerk operational: https://github.com/emberian/dregg
topical to the conversation, it is fully formally verified in lean (with some UC security reductions done in isabelle). also did this in HOL4 inspired by some work i did with ramana kumar in 2016, on reflective self-verifying self-modifying systems: https://github.com/emberian/svenvs
I took a look at dregg, I like the idea for an README-LLMS.txt. It seems like a good way to not only communicate to other LLM users (which we should be thinking more of doing effectively) but also I can imagine it’s helpful for your own new sessions with an LLM to arm them with proper context.
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...
Your example of the Italian school is well taken, although most of their results were later proven to be correct in the right setting. Severi's example is particularly egregious and I think a major reason this became a thing is Severi's refusal to course-correct and accept that some of the results were not correct. It has echoes of Mochizuki, and I fear, once you dig deeper, some issues around the initial declaration of "We've proven the Classification of Finite Simple Groups". There were many genuine gaps, and a lot of lore taken for granted. The sociology around how this happened is interesting - rushing to announce that it was done was the major mistake, it took away almost all incentive to actually write up the proofs and take them through proper peer-review. Genuine mathematical work was falsely reduced to "write up".
This is a bit reductive about what "proof" actually means in mathematics. Even in math, the kind of formal proofs that tools like Coq can automatically verify are an extreme, and lots of accepted and practiced math is not doing that. Proofs are often more abstract and even occasionally hand-wavy (for example not proving "obvious" statements or minor lemmas).
Mathematicians also occasionally build on top of unproven foundations (e.g. all popular asymmetric encryption schemes are built on top the assumption that certain problems such as integer factoring are hard, for which there is no formal proof), or at least explore both possibilities for statements with unknown truth value (e.g. you can find lots of work that explores the consequences of P = NP and/or P != NP).
However, there is a major separation between math and programs that I think mostly invalidates your proposal - most math we're talking about here is simply not applicable directly to the real world in any way. It's only studied for the interest of mathematicians. There is no real world consequence for Fermat's last theorem, for example - it was just a really interesting to prove theorem. In directly applied math, such as engineering, it is in fact much more common to work with unproven but well tested conjectures.
> In directly applied math, such as engineering, it is in fact much more common to work with unproven but well tested conjectures.
What specific areas were you thinking off? I don't recall, e.g., in numerics that things were often just unproven/conjectures, but might be subject matter specific.
Well, it's not exactly engineering, but physics often uses quite informal math. For a pretty modern example, the Dirac delta "function" was used long before it was formally described; and I have heard it said that even today String theory uses some math that is not fully formalized - though I can't say I know what specifically, so I may be wrong. Newton expressed calculus in terms of inifinitesimals (the dx notation was simply an infinitesimal delta x, not merely notation for derivation), which were not not formalized until much later, after they had already fallen out of favor and had been replaced in formal math by the delta-epsilon limits-based constructions.
Edit: one better example from modern physics - the path integral formulation, used in both string theory and other areas of QM/QFT, is not fully formalized and formally proven to work. Also, a more concrete example of a widely used but actually still unproven conjecture in string theory is the famous AdS/CFT correspondence.
It's interesting that mathematics, which is mostly recreational (I received profound disdain at the math department for asking about applications!) has such rigorous standards, but software, which entire civilizations now run on, does not.
If a piece of software is in safety-critical applications these days, it is often required to have a proof of correctness.
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.
The intelligence is only one part of the story. People need to actually go out there and do experiments. Science is not only theory, but also experimental. The best science happens when experiments show that a previously held assumption was not true. Eg the Michaelson Morley experiment where the assumption of ether was disproved. While AI is an incredibly powerful tool, it does not replace the act of observation. Thus Im sure we will still have scientists in the future and some degree of open science. There are experiments out there that by nature of their complexity need massive public coordination (CERN for instance) which in turn benefits from openness.
What is going to suck though is the ladder for juniors. We dont start out by working on big ticket problems, but usually early career researchers solve really tiny problems in a cheap way. The lowest bar for a cash strapped PhD student would be to contribute to some new theory in some way even if the student doesnt have access to equipment.
> People need to actually go out there and do experiments. Science is not only theory, but also experimental.
For biosciences and physics, sure. For mathematics? I am skeptical that your assertion applies.
Ah I see your point, I took the word science to mean bio, physics, chemistry, etc. IMO mathematics is a different discipline and not one Id consider a science, rather I see it as the language with which we express science.
If AI is somehow able to prove everything wouldn't it bypass Godel's incompleteness theorems?
> if a computer can match or surpass the collective output of the entire human scientific community the equation will change
Yes, but this is when someone reaches ASI and everything changes. For now, a good researcher can build off their discovery in a way their AI can’t.
It's not even just science. Anyone producing anything digital is now heavily incentivized to keep their wares away from the public internet, in a way we've not seen before. Drop any sample of your unique production online, and the AIs will obsolete you in days. That is a massive loss for people looking for inspiration and guidance.
> to share the load with every brain on the planet willing to give a try at science
This is what a lot of scientists love to tell themself or talk about in celebratory speeches.
The truth is: a lot of science is kept behind journal paywalls, so that only "officially approved" (in the sense of: working at a university or an governmental research institute) scientists can easily access it.
People are working on using LLMs to regenerate experimental data from the text of journal papers.
You know how I read new papers back in 1994? By going to the library, finding one in bi-annual publication list and requesting it through the University system. And it better be necessary because the uni had to pay both the catalogue and each reprint of an article. The access is most certainly easier today.
This was a lot because of the technological restrictions of that time.
Also be aware that the world wide web was actually conceived by Tim Berners-Lee for the exchange of information between scientists.
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.
Some previous submissions
HN history
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
They got into their field because they love the beauty of mathematics… As someone who isn't a mathematician, the main value I get out of math is its practical applications in science and technology
I have some sad news for you. 99% of the work mathematicians do has no immediate application, nor even an obvious path toward application in the near future. You mentioned cryptography, so for an example consider number theory: no apparent practical applications, going back thousands of years to the time of Euclid and earlier.
It’s been religion, philosophy, and recreation that have provided the motivations to study mathematics all these years, not applications. Applications have almost always followed long after the development of the pure mathematical theory. For number theory, that was the development of cryptography during WW2, millennia after the ancients laid those foundations.
Most unfortunately, it’s the truth value and the understanding which drive applications of mathematics, not the proof work itself. If the AI revolution decapitates the institution of mathematics which produces the understanding, and is unable to replace it, then the applications will cease as well.
Then you have to make sure that the AIs understand the theorems (sort of build a "world" for that - otherwise how'd there be confidence in the use of said theorems?
If cryptography didn't exist but the maths did, how'd you use it?
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.
> 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.
Well, it depends. Sometimes in math you do a lot of chipping away at a problem, and eventually a bigger result falls after all the right foundations are built. That seems to describe bottom-up building.
On the other hand when a new high-level concept becomes clear and seems to emerge like a revelation, and people start thinking in terms of those new definitions, it seems that a hundred pages worth of smaller results can fall out of it almost effortlessly. This way of describing it is more top-down.
I don't know that there's an exact parallel with software. Math keeps feeding into itself in a way that software dreams about with our ambitions of code reuse. The old Object Oriented dreams of perfectly encapsulated classes and abstractions partially worked out, but not to the degree that was envisioned.
The current situation with package managers doesn't look like a tower that keeps growing higher and higher levels of abstractions. It looks like a tower where each person wants to place one tiny brick that they call left-pad, and next year we will rebuild the lower levels instead of going higher. So the top-down and bottom-up building that we do is different. We keep rebuilding the bottom, and we don't very much like when the tower of abstractions get too tall and hard to reason about.
Well, it depends. Sometimes in math you do a lot of chipping away at a problem, and eventually a bigger result falls after all the right foundations are built. That seems to describe bottom-up building.
On the other hand when a new high-level concept becomes clear and seems to emerge like a revelation, and people start thinking in terms of those new definitions, it seems that a hundred pages worth of smaller results can fall out of it almost effortlessly. This way of describing it is more top-down.
I don't know that there's an exact parallel with software. Math keeps feeding into itself in a way that software dreams about with our ambitions of code reuse. The old Object Oriented dreams of perfectly encapsulated classes and abstractions partially worked out, but not to the degree that was envisioned.
The current situation with package managers doesn't look like a tower that keeps growing higher and higher levels of abstractions. It looks like a tower where each person wants to place one tiny brick that they call left-pad, and next year we will rebuild the lower levels instead of going higher. So the top-down and bottom-up building that we do is different. We keep rebuilding the bottom, and we don't very much like when the tower of abstractions get too tall and hard to maintain.
Does the the (,1) conjecture paper in annnals of Math say 7 years between submission and acceptance? Insane
These stories are common in math, e.g. these recently happened to me, a lowly mathematician:
1) Two and a half years with no reply from a journal (not even to emails I sent that I'd like to retract the paper so I could send it somewhere else). Then suddenly they tell me the paper is accepted.
2) One year with no reply. Then, my "anxious" collaborator sends them countless emails and gets redirected from person to person and finally an editor tells us that they decided almost immediately to reject our paper but they didn't tell us because "they hate giving bad news".
These were not top journals like Annals, but decent, prestigious ones, from whom you'd expect some professionalism.
I've had a paper unrejected from Duke. The publication process sucks
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?
Science is not about results, it is about the transmission of knowledge. So long as those AI-"sciences" are just inside AI, they are "engineering", not science.
I am not dismissing engineering (it moves the world we live in), just trying to clarify what science is.
Applied fluid dynamics works like that: noone has ever really "verified" that the finite-element method applied to some specific model does converge
Agree, but more specifically Math is clearly about a human understanding structure of things. Math is basically for humans. It's one of the main reasons understandable proof is so important.
Well, by "understanding" I mean "understanding by humans", indeed.
Engineering is used fairly loosely these days but I insist engineering ends where you have to prove theorems.
That’s a strange delineation. Engineering is essentially about designing a thing, asking whether that thing really does satisfy the desired criteria, and then iterating when it does not. Mathematical models of the world are tremendously useful to this practice—engineers don’t need to guess about many aspect of the real world: they have physics. What they want, more than anything else, is strong evidence that a property holds. Internal validity (proof) and external validity (experiment) are the best evidence that you can get—why would you throw one of those approaches away?
So what I’m most curious about is this: if there are axioms and proofs so enormous that a human could never prove them in a lifetime, but a machine can, does that make it engineering? That’s the point I’m really wondering about.
I mean, what if a human could follow every single step of the process in principle, but the sheer volume is so vast that a human can never see the whole thing—would that be engineering?
But I don’t think of that as engineering. In the future, maybe it will be called an Oracle
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.
Eh? I thought this was the main thrust of the argument: Mathematics has in fact always prized conceptual advancement and understanding over proof, despite presenting itself internally and externally as rewarding the latter. The author calls what he’s proposing “rebranding a plurimillenial project”.
The proposal needs to be larger, to education itself in all subjects. We are manufacturing too many specialist parrots without critical analysis. We need to teach how to discuss controversy and manage disagreements, and then we can start making progress.
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.
Right; this is my viewpoint too. All the "pure mathematicians" have a bleak future where AI can do all the puzzle solving better and faster. They existed in their own world elevating "theorem proving within a formal system" as the central aspect of "proper" mathematics and everything else as ancillary.
It always felt wrong to me that while the scientific method iterated starting with the "real world" viz. Observe, Measure, Hypothesize (includes modeling with mathematics), Test and Refine; pure mathematicians lost themselves in the formalization of hypothesizing/modeling and thus lost touch with mapping it to reality. The AI revolution is now showing them up.
Yes. Though even philosophy, which doesn't have the "real world" iteration that science does, arguably doesn't have the problems of pure mathematics.
Pure mathematicians create ever more abstractions and get lost in solving puzzles on how these abstractions logically relate to each other. But since these abstractions don't have any relevance outside of pure mathematics, it's an entirely self-referential game, like chess. Except that nobody confuses being a professional chess player with being a noble researcher.
Even in philosophy, at least analytic philosophy, that issue of getting lost in your own abstractions doesn't really exist. Because analytic philosophy doesn't analyze its own concepts, it analyzes the concepts that already exist in natural language. Like truth, knowledge, probability, causation, belief, desire, consciousness, rationality and so on. These concepts come from outside of philosophy, and they have independent relevance for non-philosophers.
In contrast, pure mathematics seems to be the part of mathematics that only has relevance to pure mathematicians. Similar to how a game like chess has only relevance to chess players, not to anything entirely unrelated to chess. But again, people who are into mastering some game or sport are fully aware that what they are trying to master is a self-contained game, or a sport, not something that increases the amount of human knowledge beyond that.
This might be the most interesting essay on the nature of mathematics I have ever read.
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 !
You start with instincts that are more easily ascribed to ethically-neutral or ethically-positive reasoning, and then turn them into a spurious criticism of capitalism. Case in point: in the USSR, the means of producing chairs were 100% state-controlled and not motivated by profit, but the country operated soulless production lines too.
The motivation behind all this is less "haha I want profit" and more "billions of people need chairs, approximately none of them care about the craftsmanship, so it's in our best interest to make furniture in the most resource- and labor-efficient way possible". Even if the state subsidizes the production of handcrafted chairs, the population is the poorer for it on a resource allocation basis, because we now need a million artisanal chair-makers instead of a bunch of factories.
I don't think you have it right- the analogy to woodworking and craftsmanship is a category error and probably misses the broad thrust of the essay.
The goal of a woodworker or craftsman is the production of a finished good. He's arguing that, although it's been convenient to position a mathematician as a "theorem-producer", that's never really been the aim of mathematics, and that the actual products of mathematics are some kind of "mental software"- see his references to neuroplasticity. Basically, he's saying that the goal of mathematics is to create abstract structures that allow humans to reason about increasingly complex concepts, and that the "mathematician as theorem producer" is more like a convenient fiction that mathematicians have allowed to persist for too long, and now threatens to endanger the whole practice of mathematics.
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.
Being invited to conference talks around the world is a completely normal part of being an active researcher in almost any academic field, so it doesn't register as pompous to other academics.
Yes, which makes starting with those somewhat strange as they're largely unrelated.
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.