Proof of geometric Langlands conjecture so complex almost no one can explain it | Hacker News Reader

Proof of geometric Langlands conjecture so complex almost no one can explain it

newscientist.com

63 pointsisaacfrond62 comments

If 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/

Looks like they were released in early May? Maybe we should wait for other mathematicians to validate the work?

Not 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.

I 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.

I’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.

Yeah, well, if anyone could understand something, there would be no point in having a PhD in it.

That's it true at all. A PhD is someone capable of doing research. Research requiring training doesn't mean results must be inscrutable.

It's a joke. I'll make sure to add a suitable smiley from now on :P

I think "a phd in algebra" is shorthand for "I did my doctoral research on an apocryphal subject that is only understood by a sub-sub-sub field of the mathematics research community and I wrote a thesis with a title that would simultaneously melt your brain and mean nothing to you, so I'm saying it in a way that you would kind of get more or less what my PhD was approximately about ish, with caveats".

In the same sense, I "have a PhD in AI". You have a PhD in "what could be said to be the Landlands problem itself". It happens.

Is that a good thing?

In my experience there is a strong correlation between depth of understanding and being able to communicate a topic effectively. I have encountered many technical papers that drape simple concepts in needless complexity. My area of expertise is software design and it's usually the least skilled people that produce the highest complexity. I find there is a lot of value in solving things in a way that is easy to understand.

Mathematicians could do a better job of conveying their topics, but this is really not the case. Some things are just genuinely hard, and the research frontier in mathematics is one of these. If you could produce a 5-page proof of an important theorem that currently has a 100-page proof, you would be hailed as a hero.

There’s really a lot more to it than that. There is a notion of “polite mathematics” which is independent of the difficulty of the proof.

If every step clearly follows from the prior steps it’s rather immaterial how long the proof is. Similarly a short proof with enough rabbits can achieve a kind of incomprehensibility.

What is "polite mathematics"? That sounds like "logic".

What's a "rabbit"?

A rabbit is when the mathematician presents the next step in a proof as a magician pulls a rabbit from a hat; leaving his reader to puzzle out how the trick was performed. For shorter proofs this can be delightful, but for longer ones it becomes tedious or even unmanageable.

> In my experience there is a strong correlation between depth of understanding and being able to communicate a topic effectively.

I claim that I would be able to explain some rather deep results from my area of mathematical expertise quite effectively. But for the ordinary person to understand my explanations, we would have to start with a full-time course about elemetary basics that lasts for quite some months.

On other words: just because you are able to communicate a topic effectively does not mean that the other side has the necessary background knowledge to understand your good explanations.

I fully agree.

However here we are not talking about laymen, we are talking about people with PHDs in related or exactly this field. If they can't understand it, who is left?

> However here we are not talking about laymen, we are talking about people with PHDs in related or exactly this field.

In particular in mathematics, research areas are quite isolated from each other, so even for a people from a related (sometimes even from the same) field, it typically takes a very serious effort to gain the necessary knowledge to understand a proof. This is also a reason why paper reviews take so much longer in mathematics than in many other academic disciplines.

Genuine question, does this level of complexity lead to higher rates of mistakes, such as faulty proofs passing review?

I'm asking this because in my field of expertise it's a common correlation, that the more complex and arcane a piece of code is, the lower the chance is that issues will be discovered during review. In addition the chance of issues grows superlinear with complexity, as more control flow and invariants needs to be tracked in error prone human minds.

So you can't explain your stuff to an 8 year old child like Richard Feynman insisted ?

> So you can't explain your stuff to an 8 year old child like Richard Feynman insisted ?

I can explain stuff to an 8-year old child, but a very long part of my explanation will be about bringing the child "from zero to graduate-level knowledge" in mathematics.

The solution to explaining stuff to an 8-year old child is thus not by making the material sufficiently stupid to make it understandable to a typical 8-year old, but to make the 8-year old sufficiently smart and knowledgeable to understand the topic.

I have a PhD in 'political science'. So I understand everything.

Title: this is about the geometric Langlands, not Langlands. They are related but in separate fields.

Yep; "morally" related but not technically connected. Robert Langlands is... not a fan of the name "geometric Langlands", to say the least.

Squeezed in above. Thanks!

The ABC Conjecture and Mochizuki's IUT theory comes to mind.

Forget the proof for a moment. Can anyone at least explain what the conjecture is?

https://www.youtube.com/watch?v=4dyytPboqvE

Thank 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?

Not 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.

Yeah, 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.

I 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.

It’s actually much more interesting. Category Theory is one of a number of systems that can underpin regular mathematics. The root of the tree, if you will. There exist proofs that these systems are equivalent and they’re not that hard to follow.

But there’s a lot of branches of the tree of mathematics involving extremely different constructions. What is proven here is that two branches of mathematics have a logical equivalence. Between this and other work, it’s looking increasingly like large numbers of the branches of the tree are effectively the same. This is insanely hard to understand right now, but hopefully in the future this will lead to a whole new understanding of mathematics where these correspondences are natural.

This is about the Langlands program, not geometric Langlands

dupe: https://news.ycombinator.com/item?id=40440520

does it involve monads?

There's maybe a two-to-three-order-of-magnitude difference between the difficulty of monads and the difficulty of this stuff.

Monads are just monoids in the category of endofunctors, after all.

of 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?

Complexity 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?

It'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.

Very common might vary by area. If you work near the foundations, I could see that, sure.

Of course it does. It uses category theory after all

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

I 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.

This 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.

It’s aimed at maybe a few hundred people in the world who can understand it. Maybe even few dozen.

Very 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).

That's the flaw in formal proofs, not the benefit.

The 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.

I 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.

While 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.

How 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.

I 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.

I imagine they’d only be taken to be proofs if formally verified. Admittedly formal verification needn’t guarantee comprehensibility.

I assume there will be a whole industry around refactoring these proofs for human legibility.

At least I'll be on equal grounds with something. I usually find out I've hallucinated my proofs :)

It is quite easy to come up with questions which have well-defined answers but the solution is insanely complex. Nobody guarantees that if the question is short and the answer as well, the path from A to B will be short too.

I think that’s very likely and in fact even necessary to advance the field. Proofs won’t even be stored in a human-readable format. It will just be a collection of data necessary for an automated theorem prover (or verifier in this case) to connect the truth of a formal statement back to its axiomatic basis.

I don’t see any problem with that. Most of the human work will shift to designing the meta-algorithms that efficiently search “proof space” for interesting results.

Abstract math is a human hobby. Machines doing it on their own is an interesting idea, but not satisfying to the humans. May as well conjecture whatever you want, and not worry about proof at all.

Yes, same way computers generate strategies for games that are seemingly incomprehensible at first but after further analysis humans discover deeper underlying principals that went unnoticed

It’s interesting that there are an infinite number of things to prove, but the search for which ones are interesting requires understanding.

And I wonder some about what the interesting ones have in common.

Reply on news.ycombinator.com