While the title of this question is subjective, I hope to make what I'm looking for quite concrete. The first, and main question is this: If you believe that a problem you are working on is formally undecidable, but you are not a logician, what are some ways to begin learning the tools necessary for you to try to prove undecidability? Where should one begin?

Now, for an explicit example. In ring theory one of the big open problems is called **Koethe's conjecture**. There are many equivalent ways to state the conjecture such as "The sum of two nil left ideals is still nil." Let me give another equivalent description.

Let $R=\mathbb{Z}\langle a,b\rangle$ be the free ring on two non-commuting generators. Suppose that $I$ is a left ideal of $R$, containing some power of $b$, and containing some power of every element of $Ra$. Then the conjecture asserts $I$ contains some power of $a+b$. Note that $R$ is countable, and in fact we can easily enumerate the elements of $Ra$ as $f\_1,f\_2,\ldots$.

Thus, given any sequence of positive integers $\vec{n}=\{n\_0,n\_1,n\_2,\ldots\}$, the conjecture asserts that the left ideal containing $b^{n\_0},f\_1^{n\_1},f\_2^{n\_2},\ldots$ also contains a power of $a+b$.

For some sequences $\vec{n}$ (such as eventually constant sequences), it is not difficult to compute that the conjecture is true. But in general the computations get extremely difficult. Lam says in his "First Course in Noncommutative Rings" p. 171, that there has been a 

> 
> (long-held) suspicion that the Conjecture is *false*.
> 
> 
> 

If so, then it is false for a sufficiently fast growing sequence $\vec{n}$.

However, one of the troubles here is that nobody knows how to control the behavior of $I$ for fast growing sequences $\vec{n}$, and there are also ways to modify $I$ only slightly and provably *not* produce a counter-example.

My current hunch is that the conjecture is false, but to *see* this we need tools to assert that (for fast growing vectors $\vec{n}$) the ideal $I$ stays complicated. I'm not confident that the regular tools from ZFC are sufficient to the task; but have no idea where to go from here.

One last comment: There is always the danger of fearing that a problem one is working on is formally undecidable, just because you can't immediately solve it. Because of this I haven't given up hope that there is such a solution. However, there is also the chance that some stronger set theory may provide tools to look at the problem differently, and really **that's** what I'm after.