[immibis]

Busy beavers are the machines in some size class which run the longest, then halt. They may be alternatively defined as the ones which produce the most output, then halt. Machines which obviously loop are excluded, and so are machines that non-obviously loop - for example ones that loop until they prove the Riemann hypothesis are excluded if the Riemann hypothesis is false and the proof system is consistent.