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.
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.
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).
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.
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.
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.
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.
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.
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 ?
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.
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?
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.
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.
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.
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.
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
66 comments
[ 4.2 ms ] story [ 133 ms ] threadbut is the relative difficulty, in human understanding, or a 'fundamental' difference in complexity?
surely the later is something mathematicians can and have measured?
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?
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
"rewrite in lean when" isn't really practical (at least yet).
https://people.mpim-bonn.mpg.de/gaitsgde/GLC/
Not unlike IT, medicine, or parts of software development.
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.
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.
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's a "rabbit"?
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.
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?
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.
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.
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.
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.
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.
But I see a lot of categories and functors, so I guess they use, speak and think Category Theory.
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.
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 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.