[jstogin]

I see a number of people commenting on the size of the proof (roughly 900 pages) which is not uncommon in this particular sub-field of PDEs. For context, I had the distinct privilege of studying under Sergiu Klainerman for my PhD on this topic. My own dissertation was about 600 pages. From my personal experience, I have come to understand a few factors that contribute to large proof sizes. 1. A lot of work is on inequalities involving integrals with many terms. These are difficult to express without taking up substantial space on the page. Some inequality derivations themselves might take multiple pages if you want to go step-by-step to illustrate how they are done. 2. Writing a proof of this size is not unlike building a medium-to-large size codebase. You have a lot of Theorems/Classes that need to fit together, and by employing some form of separation of concerns you can end up with something quite large and complex. 3. Verifying this kind of proof isn't usually done all at once. A lot of verification happens on the individual lemmas before they're pieced together. Once the entire paper is written, verification is more of a process where you rely on intuition for what the "hard parts" of the proof are and drilling down on those. But when writing the paper, you must of course account for all the details regardless of whether they are "easy" or "hard", and there can be many.

Having said all this, I have not read their paper and it has been 5 years since I was in this space. This is a truly remarkable accomplishment and the result of decades of hard work!

I'll end with an amusing anecdote. A fellow grad student, when deciding between U of Chicago and Princeton for his PhD program was pitched by a U of Chicago professor who once said something like "Of course you could go to Princeton and write 700 page papers that nobody reads." When this story was shared during a conversation over tea at Princeton, another professor retorted, "Or you could have gone to U Chicago to work with him and write 70 page papers that nobody reads!"

[markmiro]

If these proofs really are like codebases, wouldn't we eventually expect these proofs to be written as software?

You'd install lemmas using a package manager and then import them into your proof.

You can then install updates to proofs. Maybe someone has found the proof to be wrong, in which case you either find a different proof or invalidate the lemma so all the dependents can be invalidated automatically.

[anyfoo]

That is not too far from what proof assistants actually do.

Agda is a dependently typed language (strongly resembling Haskell in Syntax, but with a lot more Unicode) where you rarely, if ever, "run" your programs but rather just check if they "compile", i.e. type check. If it does type check, you proved what you set out to prove.

Its standard library contains a lot of stuff you'd need for basic proofs: https://agda.github.io/agda-stdlib/

[HighlandSpring]

And the individual lemmas could have author and chronology metadata attached, then you could plot the DAG as a roadmap/tech tree of sorts with an axis corresponding to time.

You'd be able to at a glance see the year a result entered public domain, who authored it, etc

One can dream

[clcaev]

Creating an extensive library of formally verified results is the goal of many systems, such as http://metamath.org/

[jstogin]

I have wondered this as well. In theory, I want to say yes. But in practice, at least in this subfield, there are so many unimportant details that might make this really difficult.

It's not a perfect analogy, but some parts of the proof feel more like neural networks than procedural algorithms. So instead of verifying the composition of two procedural algorithms g(f(x)), you have something more like g(nn(f(x))), where nn is some sort of ML model / neural network. Interestingly, we are starting to see progress in importing ML models as libraries (eg Huggingface), so maybe that can carry over someday? I don't know.

Another challenge is simply a practical one. You would need someone heavily interested in both black hole mathematics and formal proof verification to be able to do this. Both of these require years of training.

[remolueoend]

The isabelle AFP project (https://www.isa-afp.org) might be interesting to you.

[barking_biscuit]

And then you can learn about a hip new javascript front-end framework for your proofs every month on HN.

[kapv89]

Checkout leanprover

[whatshisface]

Can anyone build on results that are so hard-won and complex that understanding them is as much effort as learning the basics of some entire fields of study?

[LeifCarrotson]

Yes. That's how basically all expansion to the field of human knowledge is constructed today.

A human can only ingest and understand so much information in so much time. As Matt Might[1] eloquently described in "The Illustrated Guide to a PhD" [2], learning the basics of an entire field of study is what a bachelor's degree is for, a master's degree gives you a specialty, graduate students reading research papers like this one is how you get to the edge of human knowledge...only then can you start building on that sum of knowledge.

[1] http://matt.might.net/

[2] http://matt.might.net/articles/phd-school-in-pictures/

[btrettel]

I don't agree with that article. I previously wrote about my disagreement on HN: https://news.ycombinator.com/item?id=29141107

To summarize, a PhD often (maybe even typically) does not bring someone to the edge of human knowledge. Often a PhD gets people near it, but given the shear amount of scientific literature out there, it's difficult to know where the edge is.

[redtexture]

History PhDs often break new ground.

I believe more than a few scientific PhDs do as well, and more than a few can become journal articles, or amount to a compilation of previously successfully accepted journal articles.

This item, an outstanding PhD thesis of an outstanding historian.

Free Soil, Free Labor, Free Men: The Ideology of the Republican Party before the Civil War

Eric Foner

[jstogin]

Some graduate students will likely spend a substantial part of their PhD understanding this paper. They will learn a lot in the process, and then they can contribute by either extending the result or finding a way to simplify a part of the proof. Or if they have a (very) related interest, they may be able to adapt some of the techniques to the problem they're interested in. Slowly over time, through this process, the knowledge might diffuse to other less related areas.

[cercatrova]

Oftentimes proofs start out very complex but become simpler as time goes on and more people understand it and connect it to other existing ideas.

It is akin to refactoring a codebase after it started as a spaghetti code behemoth.

[gigatexal]

What an insane effort. And to think the peers of these folks that had to edit/accept this stuff had to check and verify the new math they came up with for the proof.

That’s my one issue — is it dubious we have to come up with new math to prove stuff? Or is that readable especially when dealing with such exotic things like black holes?

[swayvil]

Would it be possible to create a proof of a proof?

Like : Given this list of assumptions -- This list of conclusions is proven to be true.

Maybe even with a confidence rating.

Then you could package your proof inside the proofproof. Thus sparing us the effort of reading it, and maybe even make your proof more widely appreciated.

[Archelaos]

> Would it be possible to create a proof of a proof?

The sub-discipline of mathematics that deals with this is called "metamathematics". For a start see https://en.wikipedia.org/wiki/Metamathematics

[thomasahle]

In principle you could provide what's called a Probabilistically Checkable Proof. This would be a long string of bits, and a verifier would only have to sample 3 random bits to check the validity of the whole thing.

In practice we don't even make "normal" machine checkable proofs. They are just too much work. Maybe in the future when the machines are better at understanding us.

[Bolkan]

AbstractProofControllerFactoryImpl

[mensetmanusman]

Sounds like the halting problem :)

[kapv89]

600-900 pages proofs are why formalising mathematics is needed (lean)

[arcen]

Are there any tools that are used to manage all the pieces?

[lb7000]

I haven't seen any medium to large size codebases that are bug free. How do those issues get identified when it's on paper?

[Bolkan]

> 2. Writing a proof of this size is not unlike building a medium-to-large size codebase.

Is there something akin to an IDE that you guys use for this.

[momentoftop]

If the proof is that size, I'd leave it out of my thesis proper, and just provide a link to it as a stable artifact.

[auntienomen]

How do you know you don't have errors in a 600 page proof?

[tremon]

By adding 1200 pages of unit tests, of course.

[jstogin]

It probably wouldn't be too surprising if at least one error was lurking somewhere in those 900 pages. But if such an error were found, the authors would almost certainly be able to address/patch it very quickly. They have very good intuition for the "hard" parts of the problem and focus so much on those parts that it would be highly unlikely to overlook a critical error.

[Mimmy]

Thank you for sharing both the insight and the anecdote.