In this essay, Scott Aaronson describes Tibor Rado's "Busy Beaver" sequence, as follows.
... we can classify Turing machines by how many rules they have in the tape head. ... for each fixed whole number N, ... there only finitely many distinct machines with N rules. Among these machines, some halt and others run forever when started on a blank tape. Of the ones that halt, asked Rado, what’s the maximum number of steps that any machine takes before it halts?
Due to the impossibility of the halting problem, no algorithm can list all of the Busy Beaver numbers. However, apparently some Busy Beaver numbers can be and have been calculated. Aaronson describes...
... This means that no computer program could list all the Busy Beavers one by one. It doesn’t mean that specific Busy Beavers need remain eternally unknowable. And in fact, pinning them down has been a computer science pastime ever since Rado published his article. It’s easy to verify that BB(1), the first Busy Beaver number, is 1. That’s because if a one-rule Turing machine doesn’t halt after the very first step, it’ll just keep moving along the tape endlessly. There’s no room for any more complex behavior. With two rules we can do more, and a little grunt work will ascertain that BB(2) is 6. Six steps. What about the third Busy Beaver? In 1965 Rado, together with Shen Lin, proved that BB(3) is 21. The task was an arduous one, requiring human analysis of many machines to prove that they don’t halt—since, remember, there’s no algorithm for listing the Busy Beaver numbers. Next, in 1983, Allan Brady proved that BB(4) is 107.
This description suggests that "arduous" human analysis was used to analyze programs to determine halting, due to the fact that no algorithm can exist. How is human analysis not subject to the same restriction that every algorithm is, in being unable to determine halting?
Is Aaronson's description here accurate in suggesting that human reasoning is capable of determining halting, which machines are incapable of? If so, how is human analysis capable of what algorithms are not?