Ever since 1611, Johannes Kepler had suggested that the most efficient way to stack unit spheres is to arrange them in a pyramid formation. Thomas Hale managed to come up with a 300 page proof in 1998, but reviewers were only 99% certain that the proof is correct even after spending 4 years on it.
As such, in 2003, Hales began to create a computational tool that could formally verify the proofs by relying on small, easily validated series of logical statements, to bootstrap their way to long tedious proofs. Finally, in August 2014, Hales announced that he was able to computationally verify that the pyramid offered the densest packing.
"This technology cuts the mathematical referees out of the verification process," says Hales. "Their opinion about the correctness of the proof no longer matters." This would also allow us to verify the dense mathematical proofs written up in specialized fields, which few other mathematicians would be able to follow.
Imagine if one day a computer could come along and grade your solutions on Brilliant, and tell you if it's right or wrong! The community will no longer need to point out errors or flaws, and will just appreciate the proofs and echo "Well Done!"