In which computers help prove something that humans gave up on because it was too complicated.
Hales and Ferguson originally announced a proof in 1998, but the solution was so long and complicated that a team of a dozen referees spent years working on checking it before giving up.
wonderful!
wonderful!