Neat News - Neat things do happen

The boolean Pythagorean Triples problem is to answer the question whether it is possible to colour the natural numbers by two colours so that never all three numbers in a triple (a,b,c) with a² + b² = c² have the same colour. The problem has now been solved with the help of computers in a proof that originally was two hundred terabytes big, the largest proof ever generated. The Nature article states that its size corresponds roughly to all the digitized text held by the US Library of Congress.