It's probably not 10MB, but famously the groundwork to prove the statement 1+1=2 is nearly 400 pages in to principia mathematica. That's not even proving 1+1=2, it's just the set-theoretic proofs you need to EVENTUALLY get there.

Yes. But I think that misses the point.

In 1799, Paolo Ruffini published a 500 pages long proof showing that there is no closed algebraic solution for the roots of a polynomial of degree five or higher. The proof is extremely verbose and brute-force, essentially enumerating and checking hundreds of cases by hand. It is by today’s standards insignificant.

About 25 years later, Evariste Galois proved the same result in about 95% less space by describing the first general theory of groups and fields. It is considered one of the greatest contributions to mathematics of that century, not because of the result, but because its approach opened up a whole new universe of questions, methods and insight. There would be no AES encryption without Galois.

To me, Astras proof looks like Ruffinis proof.