Chaitin's elegant programs
The algorithm $B$ is described in a mildly sloppy way. You can look at it as a two-step process:


Find suitable $P_k$.
Run $P_k$.


Now, step 1 can be done one program at a time since the set of all programs is recursively enumerable and we assume that a recursive (and total) elegance tester $\mathrm{ET}$ exists. Note that we use $\mathrm{ET}$ as an oracle.

So, the algorithm is this:

def B(N,x)
  E = program_enumerator

  do
    P = E.next
    if ( length(P) &lt;= N )
      continue
  while ( !ET(P) )

  return P(x)
end


Why is this a proof? We call the underlying technique proof by contradiction. Here is what happens:


Assume that a general, total elegance checker $\mathrm{ET}$ exists.
Under this assumption, construct a (computable!) program $B$ that is equivalent to a program $P$ so that $B$ is smaller than $P$ but $\mathrm{ET}$ says that $P$ is elegant (i.e. smallest).
Since this is a contradiction, the assumption has to be false; that is, such an elegance checker can not exist.