When Johannes Kepler’s inquiry into the structure of snowflakes led him in 1611 to propose the most efficient method for stacking items in three dimensions, little did he guess that nearly 400 years would pass before his solution would be proven—nor that the proof, by mathematician Thomas Hales, would be about as long as 10,000 full-length novels. It would take “about 30 years merely to read it,” according to mathematician Ian Stewart. Not only are computers needed to create such monster proofs, Stewart says, but only computers can verify them. And that calls into question the very nature of mathematical proofs.

Ever since Euclid of Alexandria invented proofs in the third century bc, most people have gotten their introduction to them in geometry class. Later mathematicians followed Euclid’s method of writing down proofs so that others could verify  their work. There was “an unspoken assumption that the verification process could, and should, be carried out by one unaided human brain.”