Once upon a time, over 40 years ago, a horde of computer scientists descended on the West German city of Dortmund. They were competing to catch an elusive quarry — only four of its kind had ever been captured. Over 100 competitors dragged in the strangest creatures they could find, but they still fell short. The fifth busy beaver had escaped their clutches.

Of course, that slippery beast and its relatives aren’t actually rodents. They’re simple-looking computer programs that take a surprisingly long time to run. The search for these unusually active programs has connections to some of the most famous open questions in mathematics, and roots in an unsolvable problem as old as computer science itself. That’s precisely what makes the hunt so compelling. Three of the Dortmund participants summed up the prevailing attitude in a postmortem report: “Though we know we cannot win the war against the mathematical law, we would like to win a battle.”

The spiritual sequel to the Dortmund hunt began two years ago, when a graduate student named Tristan Stérin launched a website announcing the Busy Beaver Challenge. This time, the participants would cooperate, and everyone was welcome. Over time, the online community grew to include more than 20 contributors from around the world, most of them without traditional academic credentials.

Today, the team declared victory. They’ve finally verified the true value of a number called BB(5), which quantifies just how busy that fifth beaver is. They obtained the result — 47,176,870 — using a piece of software called the Coq proof assistant, which certifies that mathematical proofs are free of errors.

To read more, click here.