On topic, what is the content of this 200tb proof? Is that just a text file where each character is a bit? How many libraries of congress is this proof?

Consider the integers between 1 and 7285. To each integer i assign a boolean variable P_i. These variables encode the partition of these integers into two classes (think of P_i as encoding the statement ""the integer i belongs to the first class").

Now let $a,b,c$ be a Pythagorean triple (a^2+b^2=c^2 and 1

Finally, the claim "every triple is not monochromatic" is obtained by taking the conjuction of the Q_{a,b,c} over all triples (a,b,c) as above. It's a huge boolean expression and the goal is to show that it always evaluates to FALSE (in other words, that for any boolean assignment to all the P_i), the huge conjugation always takes the values.

The proof works by manipulating this boolean expression: it has 200TB of instructions on how to manipulate this huge boolean expressions step-by-step in ways that obviously don't change its truth value, so that at the end one of the clauses in the conjunction simply reads "FALSE", making the whole expression indeed universally false. A computer program discovered this list of manipulations, and a separate (much simpler) program can easily verify that the manipulations are of the right kind (they don't change the truth value) and that at the end of the manipulation you get a clause saying FALSE.