Well, I didn't know this:
Computer-assisted proofs too large to be directly verifiable by humansAnd how big is a 200Tb proof?:
have become commonplace, and mathematicians are familiar with computers
that solve problems in combinatorics — the study of finite discrete
structures — by checking through umpteen individual cases. Still, “200
terabytes is unbelievable”, says Ronald Graham, a mathematician at the
University of California, San Diego. The previous record-holder is
thought to be a 13-gigabyte proof2, published in 2014.
...roughly equivalent to all the digitized text held by the US Library of
Congress. The researchers have created a 68-gigabyte compressed version
of their solution — which would allow anyone with about 30,000 hours of
spare processor time to download, reconstruct and verify it — but a
human could never hope to read through it.