The Busy Beaver value S ( n ) is the maximum number of steps that an n-state 2-symbol Turing machine can perform from the all-zero tape before halting. S was historically introduced by Tibor Radó in 1962 as one of the simplest examples of an uncomputable function. We prove that S (5) = 47,176,870 using the Coq proof assistant. The proof enumerates 181,385,789 Turing machines with 5 states and, for each machine, decides whether it halts or not. Our result marks the first determination of a new Busy Beaver value in over 40 years and the first Busy Beaver value ever to be formally verified, attesting to the effectiveness of massively collaborative online research (bbchallenge.org).