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 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.
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.
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?
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.
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.
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.
Readit News
https://people.mpim-bonn.mpg.de/gaitsgde/GLC/
Deleted Comment
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.
Not unlike IT, medicine, or parts of software development.
but is the relative difficulty, in human understanding, or a 'fundamental' difference in complexity?
surely the later is something mathematicians can and have measured?
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).