Comment by daxfohl

Ideally we'd be able to get a little of both. A proof of such magnitude should likely come with new definitions that are easy to search for in the code and start to reason about independently. Even without looking at the rest of the proof, I imagine we'd be able to deduce a fair amount of the structure just by understanding the new things that are being defined, what existing theorems are being imported, and connecting the dots.

Your comment reminds me of Tao's comment on the ABC conjecture: usually with a big proof, you progressively get new tools and examples of how they can be applied to other problems. But if it's hundreds of pages of formulas that just spits out an answer at the end, that's not how math usually works. https://galoisrepresentations.org/2017/12/17/the-abc-conject...

If these provers do end up spitting out 1000-page proofs that are all calculation with no net-new concepts, I agree they'll be met with a shrug.