[HN Gopher] Monumental proof settles geometric Langlands conjecture
___________________________________________________________________
Monumental proof settles geometric Langlands conjecture
Author : jandrewrogers
Score : 185 points
Date : 2024-07-26 17:14 UTC (1 days ago)
(HTM) web link (www.quantamagazine.org)
(TXT) w3m dump (www.quantamagazine.org)
| proof_by_vibes wrote:
| 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.
| vinnyvichy wrote:
| 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..
| proof_by_vibes wrote:
| 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!
| downvotetruth wrote:
| Prior:
|
| https://news.ycombinator.com/item?id=40280760
|
| https://news.ycombinator.com/item?id=40453822
| paulpauper wrote:
| 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.
| antognini wrote:
| 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 Faergeman 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."
| calf wrote:
| Are they tenured professors?
| lanstin wrote:
| They are now :)
| senderista wrote:
| 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
| bdjsiqoocwk wrote:
| 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.
| leephillips wrote:
| 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.
| EVa5I7bHFq9mnYK wrote:
| Interesting, Alexander Friedmann, another notable solver of
| Einstein equations, also fought in WWI, though on Russian
| side :)
| bdjsiqoocwk wrote:
| Similar for the Choleski decomposition. Also artillery
| officer in WWI. Died in battle.
| chinabison wrote:
| Jean LeRay invented sheaf theory while he was a POW in
| Austria in WWII.
| anthomtb wrote:
| 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?
| xanderlewis wrote:
| 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.
| seanhunter wrote:
| 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)
| slanderaan01 wrote:
| 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.
| seanhunter wrote:
| 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
| bdjsiqoocwk wrote:
| String theory is still the only self consistent theory of
| quantum physics.... I'd say that's extremely successful.
| defrost wrote:
| 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.
| bdjsiqoocwk wrote:
| > 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.
| jerf wrote:
| "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.
| bdjsiqoocwk wrote:
| 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.
| ur-whale wrote:
| Is there a machine-verifiable version ?
|
| I mean ... 800 pages, I'd say the benefit of the doubt applies.
| msm_ wrote:
| 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.
| isotypic wrote:
| 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.
| dylanwenzlau wrote:
| Article and interspersed visuals were a pleasant learning
| experience. I'm not caught up on mathematics as much as I'd like
| to be..
___________________________________________________________________
(page generated 2024-07-27 23:11 UTC)