World's Largest Computer-Generated Math Proof

Computer scientist Marijn Heule and his colleagues have solved a decades-old math challenge known as the boolean Pythagorean Triples problem (BPTP) and, in the process, created the largest mathematical proof ever, at a whopping 200 terabytes.

The achievement had some writers pondering whether solving math problems with computers is really even mathematics. Others speculated on whether computers might eventually replace human mathematicians altogether.

In the early 1980's, one of the world's leading mathematicians, Ronald Graham posed the BPTP and offered a $100 prize for the first person to solve it. Solving the problem by brute force would have required checking more possible partitions than atoms in the universe. Heule, a research scientist at the University of Texas at Austin, and his colleagues used a combination of techniques to limit the search to about 1 trillion possibilities. It took them about two days on UT Austin's Stampede supercomputer to find the answer.

Stampede, among the fastest in the world, is operated by the Texas Advanced Computing Center, which recently unveiled plans to build the even faster Stampede 2.

"I was surprised that you could do it," says Graham, referring to current limits on the power of supercomputers. "It just took so much computation and so many clever ideas."

Heule will present the team's work at the International Conference on Theory and Applications of Satisfiability Testing (SAT 2016) in July, where they will receive the conference's best paper award. His co-authors are Oliver Kullmann of Swansea University, UK, and Victor Marek of the University of Kentucky in Lexington.

"The smartest mathematicians were unable to prove this for decades, but our algorithm was able to solve the problem in just two days," says Heule.

The proof alone is so large that a human could never read and evaluate it fully in their lifetime. Instead, another computer program was used to verify the proof.

One possible application of their method could be in making microchip designs more reliable. Chip designers often start out with a design that is straightforward, but slow. Then many engineers work to improve the design, but each optimization can potentially introduce errors. Validating that the process was correct has traditionally been hard. It's necessary to check that no change could cause the circuit to malfunction. Luckily, such a validation can be translated into a "satisfiability problem" – the same way of formulating problems that Heule and his team used to solve the BPTP.

Read more about the achievement in these press accounts:

Two-hundred-terabyte maths proof is largest ever, Nature

Will computers replace humans in mathematics?, The Conversation

World's Largest Math Proof Takes Up 200 Terabytes, Popular Mechanics

Computer generated math proof is largest ever at 200 terabytes, Phys.org

Largest Math Proof In The World Solved In 2 Days, 200 Terabytes In Size, Tech Times