7 ms·
Proof of geometric Langlands conjecture so complex almost no one can explain it
- billsmithaustin 2y ago[flagged]
- jacknews 2y agodoes it involve monads?
- gjm11 2y agoThere's maybe a two-to-three-order-of-magnitude difference between the difficulty of monads and the difficulty of this stuff.
- mrtranscendence 2y agoMonads are just monoids in the category of endofunctors, after all.
- jacknews 2y agoof course my post was slightly a joke but is the relative difficulty, in human understanding, or a 'fundamental' difference in complexity? surely the later is something mathematicians can and have measured?
- tux3 2y agoComplexity has different meanings. People don't generally go and assign objective metrics of complexity to proofs, besides how long it is. You could try to draw the stack of abstractions necessary to understand the proof and see how high it stacks, and you could try to call that fundamental complexity, but I don't think many people would be happy with that. So yes, it's a difficulty in human understanding. What else could it be?
- thaumasiotes 2y agoIt's very common to track how many different axioms are needed for some result, and consider results with lower requirements to be more fundamental. "Less complex", probably not so much, but the issue is something that a number of people care about.
- tux3 2y agoVery common might vary by area. If you work near the foundations, I could see that, sure.
- nextaccountic 2y agoOf course it does. It uses category theory after all https://people.mpim-bonn.mpg.de/gaitsgde/GLC/Loc.pdf https://people.mpim-bonn.mpg.de/gaitsgde/GLC/Loc.pdf (the second paper, more than 400 pages), ctrl+f monad It's not a lot of monads. There are wayyy more functors for example
- Pet_Ant 2y agoI mean, I guess that's the benefit of formal proofs? You don't need to "understand" it to know that it's true. Just going line-by-line and if checks out you are good. The notion of "understanding" gets the "shut up and calculate" thrown at it.
- auntienomen 2y agoThis is a 5 paper long argument aimed at other mathematicians. It's a formal proof in the sense that it's standard math talk, but not a formally verifiable proof that could be, e.g., machine checked.
- p1esk 2y agoIt’s aimed at maybe a few hundred people in the world who can understand it. Maybe even few dozen.
- qsort 2y agoVery few proofs in actual professional mathematics are written in a formal proof structure where what you suggest is actually possible. You definitely need to understand the underlying ideas to follow along. "rewrite in lean when" isn't really practical (at least yet).
- lupire 2y agoThat's the flaw in formal proofs, not the benefit.
- gjm11 2y agoThe point of a proof is very much not just that it enables you to know that the thing is true, but also to give insight into why it's true. (And hence, e.g., what other related things are likely to be true and how one might prove them.) A 100% incomprehensible proof gives no such insight; a merely-somewhat-incomprehensible proof gives less insight than a more comprehensible proof could.
- isaacfrond 2y agoIf anybody is interested, here are the papers themselves. I wish you a lot of luck (I have a phd in algebra, but it is unintelligble to me). https://people.mpim-bonn.mpg.de/gaitsgde/GLC/ https://people.mpim-bonn.mpg.de/gaitsgde/GLC/
- zero-sharp 2y agoLooks like they were released in early May? Maybe we should wait for other mathematicians to validate the work?
- analog31 2y agoNot just to validate, but to explain. There are plenty of cases where the earliest descriptions of a discovery required further work to develop a more convenient notation and language for use by non-specialists. Algebra, calculus, and electrodynamics come to mind. As time progresses, a broader range of people are able to understand the content.
- zyklu5 2y agoI don't know what a phd in "algebra" means but I don't understand how anyone with a phd in any part of mathematics can find this unintelligibility surprising. I have a phd in what could be said to be the langlands program itself and I am not at all surprised I can't follow this result.
- TheNewsIsHere 2y agoI’ve always been amused that the The Princeton Companion to Mathematics, edited by Timothy Growers, amusingly notes in the introduction that for the mathematician reader it may come to pass that they may not easily understand the works of others on different areas of mathematics. Not unlike IT, medicine, or parts of software development.
- YeGoblynQueenne 2y agoYeah, well, if anyone could understand something, there would be no point in having a PhD in it.
- boilerupnc 2y agohttps://archive.is/eI9rb https://archive.is/eI9rb
- munchler 2y agoForget the proof for a moment. Can anyone at least explain what the conjecture is?
- zero-sharp 2y agohttps://www.youtube.com/watch?v=4dyytPboqvE https://www.youtube.com/watch?v=4dyytPboqvE
- munchler 2y agoThank you. Watching it now. Does the Langlands program compete with Category Theory as being the grand unified theory of math, or are they not really comparable?
- moi2388 2y agoNot a mathematician. Afaik category theory is more like an alternative to set theory. Langlands is more like a bridge between higher level mathematics, allowing you to transform hard problems in geometry to harmonic analysis and vice versa, and so far specifically these fields only.
- auntienomen 2y agoYeah, category theory is a framework for describing mathematical structure. It's not vacuous -- there are mathematical structures which don't fit into the framework and there are some theorems about what properties a category has. But category theory doesn't do that much on its own. The geometric Langlands conjectures are a _lot_ more specific, and a lot more focused. They're a big deal, because they're a toy model for the arithmetic Langlands conjectures, which are a generalization of the machinery that proved Fermat's Last Theorem and would give an effective method for dealing with a lot of number theory problems.
- hackandthink 2y agoI do not know anything about the Langlands program. But I see a lot of categories and functors, so I guess they use, speak and think Category Theory.
- tatrajim 2y agoThe ABC Conjecture and Mochizuki's IUT theory comes to mind.
- VladimirGolovin 2y agoI feel that long, unexplainable, hard-to-comprehend proofs may become commonplace when we get to AIs that are capable of discovering new proofs on their own.
- rowanG077 2y agoWhile unsatisfying from an "I solved this riddle" perspective I still think that's a great thing because it will open up a lot of stuck fields.
- fweimer 2y agoHow so? You can just assume that some conjecture is true and proceed with your work. (For some conjectures that is acceptable, for others, not so much.) An interesting proof would have to show something more than just the truth: maybe it's constructive and shows how to compute something, or it shows a connection between fields previously seen as barely related. Or it uses a new trick or language that could be applied elsewhere. But I think all that requires that the proof is a bit more than transparent than just having a formally verifiable representation.
- rowanG077 2y agoI expect that we will move in a direction that all proof. Not just steps is done by computers. The human input remaining is just to ask it what to prove.
- eynsham 2y agoI imagine they’d only be taken to be proofs if formally verified. Admittedly formal verification needn’t guarantee comprehensibility.
- Pet_Ant 2y agoI assume there will be a whole industry around refactoring these proofs for human legibility.
- 2y ago
- joppy 2y agoTitle: this is about the geometric Langlands, not Langlands. They are related but in separate fields.
- deleted 2y ago[deleted]
- ggddv 2y ago[dead]
- bookofjoe 2y agodupe: https://news.ycombinator.com/item?id=40440520 https://news.ycombinator.com/item?id=40440520