a proof that L_min is not in coRE? Define $L_{min}$ to be the language of all minimal Turing machines, in some standard encoding. (A Turing Maching is minimal if it has the shortest encoding among all the TMs recognizing the same language.) Sipser gives a slick proof that $L_{min}$ is not a Recursively Enumerable (RE) language. The argument goes like this: suppose to the contrary that $L_{min}$ is in RE, with some enumerator $E$. Define the Turing machine $B$, which obtains its own description via the recursion theorem, waits until $E$ generates a program $C$ that is longer than $B$, and then simulates the behavior of $C$. The contradiction results from the assumption that $E$ only generates minimal programs and the construction of $B$ as a program that's shorter than some "minimal" program.
Now I want to show that $L_{min}$ is not in coRE (meaning that its complement is not in RE). Any ideas?
 A: This is a problem with a surprisingly unique history. See the survey

Marcus Schaefer: A guided tour of minimal indices and shortest descriptions. Arch. Math. Log. 37(8): 521-548 (1998)

for more discussion. A proof that the problem is not coRE can be extracted from page 6 of that survey. For convenience I will give a self-contained argument here. Unfortunately it is not as simple as the "not-RE" proof!
We will show a Turing reduction from $L_{ALL}$ = { $ M~|~L(M) = \Sigma^{\star} $} to $L_{min}$, which suffices since $L_{ALL}$ is complete for the second level of the arithmetic hierarchy (implying it is not coRE). Intuitively, this means that given an oracle for $L_{min}$ we could decide the halting problem for machines which have oracles to the halting problem. A coRE language cannot have this property. 
Let $\hat{M}$ be the lexicographically first machine that accepts no inputs, under some encoding of machines. 
First, we observe that given an oracle for $L_{min}$, we can effectively determine whether $M(M)$ halts or not, for a given $M$. (Recall this is enough to determine whether $M(x)$ halts or not, for given $M$, $x$.)
Define a machine $N_M$ which on input $t$, simulates $M(M)$ for up to $t$ steps and halts iff the simulation halts. To determine if $M(M)$ halts, make a list ${\cal L}$ of all machines $M' \neq \hat{M}$ with $M' \leq N_M$ such that $M' \in L_{min}$. This list can be computed using an oracle for $L_{min}$. Observe that all such machines accept at least one input, since we excluded $\hat{M}$ and they are all minimal. Via dovetailing, we can effectively find integers $t'$ such that each $M'(M')$ halts in $t'$ steps. Let $t''$ be the largest such $t'$. Then $M(M)$ halts iff $M(M)$ halts in at most $t''$ steps. 
Now that we can decide the halting problem, we turn to computing a function version of $L_{min}$: given an oracle for $L_{min}$, we can output the minimum equivalent machine $M'$ to the input $M$. If $M \in L_{min}$ this is easy. Otherwise we make a list ${\cal L}$ of all machines that are in $L_{min}$ and are smaller than $M$. Then we begin to compute, for increasing inputs $x$, bit tables indicating the accept/reject behavior of all machines in ${\cal L}$, on the inputs seen so far. (We can do this because we can solve the halting problem with the oracle!) When we find that a machine $M''$ differs on an input from $M$, we remove it from ${\cal L}$. If $M$ is not minimal, there will eventually be only one machine $M'$ left which has not yet differed from $M$, since all machines in ${\cal L}$ are minimal. If $M$ is not minimal then this $M'$ must be the minimum machine.
Finally, we define a machine $N$ that recognizes $L_{ALL}$ with an oracle for $L_{min}$. Let $M_{ALL}$ be the minimum Turing machine that accepts everything. If the input $M$ is less than $M_{ALL}$, output NO. ($M$ must reject something.) Otherwise compute the minimum machine equivalent to $M$. If $M = M_{ALL}$ then output YES otherwise output NO. Note $L(N) = L_{ALL}$.
