This is exciting news! Though, there is more than just the math that needs to be done here. Namely, mathematicians not only need to formalize a concise language to bridge the gap with modern conformal field theory, but they will also need a way to understand the computability of models based on this system. And yet, there is also the human factor: namely, there needs to be an effort to sell this paradigm to existing theorists, which will require substantial effort.
Can you say more about computability of "conformal models" in the Langlands context (beyond vibes, perhaps cites)? In my understanding, "conformal models" are by construction computable..
Oops, yeah, my bad. I've been doing a deep dive into lean4 and ended up conflating the use of the term computability from that context. Sorry, for the confusion!
I'm curious what applications there might be if any in number theory. If I recall, langlands had motivations from string theory concepts which ultimately wasn't as successful as hoped in physics.
I'm not sure that's true. My quick searching around is that the first paper proposing strings as a possible description of space and time is Nambu, Nielssen and Susskind in 1969 whereas Langlands first stated his conjectures in his letter to Andre Weil in 1967[1] (ie before string theory had even really kicked off mathematically which didn't happen until Ed Witten got involved in the 1980s). In his letter, Langlands seems to motivate the conjectures entirely from abstract algebra and topology (although this is way above my mathematical pay grade at the moment so I'd be more than happy to accept I misunderstand).
Not particularly, it's so open ended it describes an enormous landscape of possible universes and lacks any specific testable predictions for our universe.
Unless it's been firmed up a great deal in recent times.
> lacks any specific testable predictions for our universe.
Predicts that special relativity holds up at all scales (check, according to all evidence so far), predicts general relativity at low energy scales (check).
So it's false that it has no testable predictions. None of this happened "in recent times" though, it's been understood for a long time.
"No testable predictions" is shorthand for "makes no testable prediction that don't match our other theories, making it impossible to distinguish between string theory and relativity+QM". We know the latter doesn't really work, but without the ability to distinguish, it isn't clear that string theory "works" either. It really needs a solid new testable prediction.
If you grant arbitrarily advanced technology then "testable predictions" absolutely do exist, most immediately on the cross sections of basically every particle. We can't perform such experiments now, but that's a problem with the technology, not with the theory.
Imagine if someone had said 30 years ago that the "higgs boson theory" is a failure because we couldn't then perform the experiments to detect it.
This comparison is not really fair. On the one hand you have the prediction of a scalar excitation with a lot of restrictions (cosmology and naturalness). On the other hand you have a giant framework that can predict or fit almost anything.
Don't get me wrong, I still regard string theory as a big success. It taught us a lot about mathematics and field theories in the last decades.
However the predictive nature is basically non-existant so far.
Nonsense. It can't predict everyone, in particular it won't predict special relativity bring violated.
In addition you haven't addressed the main point here which is that when some people say "can predict" they mean "in principle it can predict" whereas other mean "can predict today with currently available technological means". Regarding the former: yes it can. I already gave the example of one such prediction, but here's another one: all particles niches have stringy modes in their spectra. Regarding the later: maybe, but thats a problem with our technology, not with the theory.
I feel this conservation is going in circles already.
Just because they are not mainstream, you definitely can have lorentz violation in string theory [0]. Spontaneous symmetry breaking can lead to induced finsler geometries, which can basically have multiple light cones (when there was the "faster than light neutrinos" result on the table. Some people used finsler spacetime to explain them).
So you made your prediction only by choosing an axiom.
There is a reason that even some proponents of string theory call it the theory of anything.
Neither does anybody else. Testable means something like testable today or in the designable future and it always has.
As for the fact this may mean a true theory is not testable today even though some hypothetical technology in the hypothetical future wielded by hypothetical beings could hypothetically resolve the problem, well, welcome to the universe we live in. This is not special pleading applied only to string theory. It's evenly applied to everything. It's just that string theory gets hit by this particularly hard, although not uniquely so (to the best of my knowledge, loop quantum gravity is also rather short on testable predictions). The only utility of quadruply hypothetical advances is to science fiction authors. And I've greatly enjoyed many such stories. But it's important to distinguish between science fiction and what we can do in reality.
No nontrivial (by modern standards) proof has a machine-verifiable version. Math is just too huge.
And (my hot take:) the formal correctness is important, but not really that important in math. Sure, we hope the proofs are correct, but the idea why the proofs are correct is often more important. Humans are not a formal verification machines, and we're often interested in why something is true (and when exactly, i.e. how does it generalise), instead of just asking a binary question. So taking this into account, even if there are holes in the current argument, the important thing is that the experts believe they can be fixed, and the insight we gained along the way.
Edit: I want to back my hot take a little:
* The four color theorem is famous for being the first major theorem to be proven using a computer (using exaustive search on a large search space - too large for human to verify). This was very controversial for the time (maybe still is), because we gained no insight into the problem! Exhaustive search doesn't begin to explain why this is - or is not - the case.
* Even more perversely, It's possible that ABC conjecture was proven in 2012 by Mochizuki. But the proof is very hard to read (very briefly: basically nobody understands it, and Mochizuki was - supposedly - very non-cooperative and refused to answer questions. Some experts claimed holes but their concerns were - quite rudely - dismissed as misunderstanding). Now we live in a split world, where most of the world consider the conjecture unproven (because we can't understand it and learn from it), but some universities consider it proven (because Mochizuki is an expert, and nobody was able to find a mistake and convince the world they're right). In other words, it's a mess.
In both cases, the problem was that we care about understanding the problem, not about just asserting something is true or false.
What exactly do you mean by non-trivial/modern standards? While certainly the largest and most complicated theorems are currently out of reach of proof verifiers, there isn't a shortage of usage of them to prove important/modern theorems (of course certain fields are much more developed/more amenable to verification than others).
I do largely agree that formal correctness within mathematics is not as important as it may seem, though this doesn't mean formal verification of a proof is completely orthogonal to understanding it - you can't formally verify something without really understanding the proof in the first place.
How do people even find the time to work on this stuff without being distracted by life, family, and everything else? I think this is why so many of these people are in Europe. America is too chaotic and full of obligations and distractions to do serious academic work.
> The solution for these irreducible representations came to Raskin at a moment when his personal life was filled with chaos. A few weeks after he and Færgeman posted their paper online, Raskin had to rush his pregnant wife to the hospital, then return home to take his son to his first day of kindergarten. Raskin’s wife remained in the hospital until the birth of their second child six weeks later, and during this time Raskin’s life revolved around keeping life normal for his son and driving in endless loops between home, his son’s school and the hospital. “My whole life was the car and taking care of people,” he said.
> He took to calling Gaitsgory on his drives to talk math. By the end of the first of those weeks, Raskin had realized that he could reduce the problem of irreducible representations to proving three facts that were all within reach. “For me it was this amazing period,” he said. His personal life was “filled with anxiety and dread about the future. For me, math is always this very grounding and meditative thing that takes me out of that kind of anxiety.”
"If I'm designing a Research Institute, would the ideal design be something where you have babies screaming, and people are sleep-deprived, and you know, and are bombarded with responsibilities, and then they would produce better research?"
I couldn't from that quote understand Knuths view.
I have however the impression that some distractions of life are more fundamental than others. If the distraction is that you might not have food tomorrow or you fear for your safety, indeed I doubt you can focus on research. However other things like babies crying and "responsibilities" are only a distraction if you let them. My mental model is that "doing research" is somewhere is Maslow's pyramid which is not the bottom, but it's not as high up as most people would expect either. I'd like to hear other people's thoughts.
No, a baby crying is often a duty. If you’re the only responsible adult, you need to deal with that. The only people who get to dodge that responsibility are ones with very supportive partners or enough disposable income to pay for a nanny.
By my count at least four of the researchers are employed by American universities and therefore most likely live somewhere in the United States.
And "this stuff" to which you refer is the intended output of their full time jobs*. So presumably, they find time to work on it in the same way a software developer finds time to write code. You just sit down and do it, because you are being paid to do it.
*Did I miss something about how these papers were developed in their spare time?
Karl Schwarzschild found the first exact solutions to Einstein’s gravitational field equations (general theory of relativity) while serving in the trenches in WWI, firing artillery at the Russians.
In the article one of the authors of the proof describes a key breakthrough as happening when he contracted covid and was thereby forced to spend 3 months in bed with nothing to do but think.
As an aside, Europeans have families, lives, distractions etc just like people in the US. Source: have lived in Europe for 30+ years. Have a family and lots of distractions. Have not proved any major mathematical theorems. (yet I suppose- there's still time)
Mathematical research (as far as I know) requires significant amounts of ‘time off’ just pondering and meditating on ideas as much as it requires time sitting at a desk concentrating on a paper or working through things on paper. A lot of people have said their best work was done whilst standing waiting for a bus, in the shower, walking in the woods …and so on.
This is exciting news! Though, there is more than just the math that needs to be done here. Namely, mathematicians not only need to formalize a concise language to bridge the gap with modern conformal field theory, but they will also need a way to understand the computability of models based on this system. And yet, there is also the human factor: namely, there needs to be an effort to sell this paradigm to existing theorists, which will require substantial effort.
Can you say more about computability of "conformal models" in the Langlands context (beyond vibes, perhaps cites)? In my understanding, "conformal models" are by construction computable..
Oops, yeah, my bad. I've been doing a deep dive into lean4 and ended up conflating the use of the term computability from that context. Sorry, for the confusion!
Prior:
https://news.ycombinator.com/item?id=40280760
https://news.ycombinator.com/item?id=40453822
I'm curious what applications there might be if any in number theory. If I recall, langlands had motivations from string theory concepts which ultimately wasn't as successful as hoped in physics.
I'm not sure that's true. My quick searching around is that the first paper proposing strings as a possible description of space and time is Nambu, Nielssen and Susskind in 1969 whereas Langlands first stated his conjectures in his letter to Andre Weil in 1967[1] (ie before string theory had even really kicked off mathematically which didn't happen until Ed Witten got involved in the 1980s). In his letter, Langlands seems to motivate the conjectures entirely from abstract algebra and topology (although this is way above my mathematical pay grade at the moment so I'd be more than happy to accept I misunderstand).
[1] https://publications.ias.edu/rpl/section/21 and https://publications.ias.edu/sites/default/files/letter-to-w... in particular
String theory is still the only self consistent theory of quantum physics.... I'd say that's extremely successful.
Not particularly, it's so open ended it describes an enormous landscape of possible universes and lacks any specific testable predictions for our universe.
Unless it's been firmed up a great deal in recent times.
> lacks any specific testable predictions for our universe.
Predicts that special relativity holds up at all scales (check, according to all evidence so far), predicts general relativity at low energy scales (check).
So it's false that it has no testable predictions. None of this happened "in recent times" though, it's been understood for a long time.
"No testable predictions" is shorthand for "makes no testable prediction that don't match our other theories, making it impossible to distinguish between string theory and relativity+QM". We know the latter doesn't really work, but without the ability to distinguish, it isn't clear that string theory "works" either. It really needs a solid new testable prediction.
If you grant arbitrarily advanced technology then "testable predictions" absolutely do exist, most immediately on the cross sections of basically every particle. We can't perform such experiments now, but that's a problem with the technology, not with the theory.
Imagine if someone had said 30 years ago that the "higgs boson theory" is a failure because we couldn't then perform the experiments to detect it.
This comparison is not really fair. On the one hand you have the prediction of a scalar excitation with a lot of restrictions (cosmology and naturalness). On the other hand you have a giant framework that can predict or fit almost anything.
Don't get me wrong, I still regard string theory as a big success. It taught us a lot about mathematics and field theories in the last decades. However the predictive nature is basically non-existant so far.
Nonsense. It can't predict everyone, in particular it won't predict special relativity bring violated.
In addition you haven't addressed the main point here which is that when some people say "can predict" they mean "in principle it can predict" whereas other mean "can predict today with currently available technological means". Regarding the former: yes it can. I already gave the example of one such prediction, but here's another one: all particles niches have stringy modes in their spectra. Regarding the later: maybe, but thats a problem with our technology, not with the theory.
I feel this conservation is going in circles already.
Just because they are not mainstream, you definitely can have lorentz violation in string theory [0]. Spontaneous symmetry breaking can lead to induced finsler geometries, which can basically have multiple light cones (when there was the "faster than light neutrinos" result on the table. Some people used finsler spacetime to explain them).
So you made your prediction only by choosing an axiom.
There is a reason that even some proponents of string theory call it the theory of anything.
[0] https://arxiv.org/abs/0708.2250
"If you grant arbitrarily advanced technology"
I don't, thus neatly resolving your issue.
Neither does anybody else. Testable means something like testable today or in the designable future and it always has.
As for the fact this may mean a true theory is not testable today even though some hypothetical technology in the hypothetical future wielded by hypothetical beings could hypothetically resolve the problem, well, welcome to the universe we live in. This is not special pleading applied only to string theory. It's evenly applied to everything. It's just that string theory gets hit by this particularly hard, although not uniquely so (to the best of my knowledge, loop quantum gravity is also rather short on testable predictions). The only utility of quadruply hypothetical advances is to science fiction authors. And I've greatly enjoyed many such stories. But it's important to distinguish between science fiction and what we can do in reality.
Indeed. Ptolemaic models of planetary movement work fine if you add enough variables.
You win two additional epicycles for that comment kind peer.
Article and interspersed visuals were a pleasant learning experience. I'm not caught up on mathematics as much as I'd like to be..
Is there a machine-verifiable version ?
I mean ... 800 pages, I'd say the benefit of the doubt applies.
No nontrivial (by modern standards) proof has a machine-verifiable version. Math is just too huge.
And (my hot take:) the formal correctness is important, but not really that important in math. Sure, we hope the proofs are correct, but the idea why the proofs are correct is often more important. Humans are not a formal verification machines, and we're often interested in why something is true (and when exactly, i.e. how does it generalise), instead of just asking a binary question. So taking this into account, even if there are holes in the current argument, the important thing is that the experts believe they can be fixed, and the insight we gained along the way.
Edit: I want to back my hot take a little:
* The four color theorem is famous for being the first major theorem to be proven using a computer (using exaustive search on a large search space - too large for human to verify). This was very controversial for the time (maybe still is), because we gained no insight into the problem! Exhaustive search doesn't begin to explain why this is - or is not - the case.
* Even more perversely, It's possible that ABC conjecture was proven in 2012 by Mochizuki. But the proof is very hard to read (very briefly: basically nobody understands it, and Mochizuki was - supposedly - very non-cooperative and refused to answer questions. Some experts claimed holes but their concerns were - quite rudely - dismissed as misunderstanding). Now we live in a split world, where most of the world consider the conjecture unproven (because we can't understand it and learn from it), but some universities consider it proven (because Mochizuki is an expert, and nobody was able to find a mistake and convince the world they're right). In other words, it's a mess.
In both cases, the problem was that we care about understanding the problem, not about just asserting something is true or false.
What exactly do you mean by non-trivial/modern standards? While certainly the largest and most complicated theorems are currently out of reach of proof verifiers, there isn't a shortage of usage of them to prove important/modern theorems (of course certain fields are much more developed/more amenable to verification than others).
* https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/ discusses a few recent usages in recent papers and the author's grant to formalize Fermat's last theorem.
* The liquid tensor experiment (https://www.quantamagazine.org/lean-computer-program-confirm...)
* Feit-Thompson was formalized in 2012.
I do largely agree that formal correctness within mathematics is not as important as it may seem, though this doesn't mean formal verification of a proof is completely orthogonal to understanding it - you can't formally verify something without really understanding the proof in the first place.
How do people even find the time to work on this stuff without being distracted by life, family, and everything else? I think this is why so many of these people are in Europe. America is too chaotic and full of obligations and distractions to do serious academic work.
The article does in fact discuss precisely this:
> The solution for these irreducible representations came to Raskin at a moment when his personal life was filled with chaos. A few weeks after he and Færgeman posted their paper online, Raskin had to rush his pregnant wife to the hospital, then return home to take his son to his first day of kindergarten. Raskin’s wife remained in the hospital until the birth of their second child six weeks later, and during this time Raskin’s life revolved around keeping life normal for his son and driving in endless loops between home, his son’s school and the hospital. “My whole life was the car and taking care of people,” he said.
> He took to calling Gaitsgory on his drives to talk math. By the end of the first of those weeks, Raskin had realized that he could reduce the problem of irreducible representations to proving three facts that were all within reach. “For me it was this amazing period,” he said. His personal life was “filled with anxiety and dread about the future. For me, math is always this very grounding and meditative thing that takes me out of that kind of anxiety.”
Quote from Knuth:
"If I'm designing a Research Institute, would the ideal design be something where you have babies screaming, and people are sleep-deprived, and you know, and are bombarded with responsibilities, and then they would produce better research?"
https://github.com/kragen/knuth-interview-2006
I couldn't from that quote understand Knuths view.
I have however the impression that some distractions of life are more fundamental than others. If the distraction is that you might not have food tomorrow or you fear for your safety, indeed I doubt you can focus on research. However other things like babies crying and "responsibilities" are only a distraction if you let them. My mental model is that "doing research" is somewhere is Maslow's pyramid which is not the bottom, but it's not as high up as most people would expect either. I'd like to hear other people's thoughts.
No, a baby crying is often a duty. If you’re the only responsible adult, you need to deal with that. The only people who get to dodge that responsibility are ones with very supportive partners or enough disposable income to pay for a nanny.
Are they tenured professors?
They are now :)
By my count at least four of the researchers are employed by American universities and therefore most likely live somewhere in the United States.
And "this stuff" to which you refer is the intended output of their full time jobs*. So presumably, they find time to work on it in the same way a software developer finds time to write code. You just sit down and do it, because you are being paid to do it.
*Did I miss something about how these papers were developed in their spare time?
Karl Schwarzschild found the first exact solutions to Einstein’s gravitational field equations (general theory of relativity) while serving in the trenches in WWI, firing artillery at the Russians.
Interesting, Alexander Friedmann, another notable solver of Einstein equations, also fought in WWI, though on Russian side :)
Similar for the Choleski decomposition. Also artillery officer in WWI. Died in battle.
Jean LeRay invented sheaf theory while he was a POW in Austria in WWII.
In the article one of the authors of the proof describes a key breakthrough as happening when he contracted covid and was thereby forced to spend 3 months in bed with nothing to do but think.
As an aside, Europeans have families, lives, distractions etc just like people in the US. Source: have lived in Europe for 30+ years. Have a family and lots of distractions. Have not proved any major mathematical theorems. (yet I suppose- there's still time)
Mathematical research (as far as I know) requires significant amounts of ‘time off’ just pondering and meditating on ideas as much as it requires time sitting at a desk concentrating on a paper or working through things on paper. A lot of people have said their best work was done whilst standing waiting for a bus, in the shower, walking in the woods …and so on.