What is the shortest program for which halting is unknown? In short, my question is:

What is the shortest computer program for which it is not known whether or not the program halts?

Of course, this depends on the description language; I also have the following vague question:

To what extent does this depend on the description language?

Here's my motivation, which I am sure is known but I think is a particularly striking possibility for an application to mathematics:
Let $P(n)$ be a statement about the natural numbers such that there exists a Turing machine $T$ which can decide whether $P(n)$ is true or false.  (That is, this Turing machine halts on every natural number $n$, printing "True" if $P(n)$ is true and "False" otherwise.)  Then the smallest $n$ such that $P(n)$ is false has low Kolmogorov complexity, as it will be printed by a program that tests $P(1)$, then $P(2)$, and so on until it reaches $n$ with $P(n)$ false, and prints this $n$.  Thus the Kolmogorov complexity of the smallest counterexample to $P$ is bounded above by $|T|+c$ for some (effective) constant $c$.  
Let $L$ be the length of the shortest computer program for which the halting problem is not known.  Then if $|T|+c < L$, we may prove the statement $\forall n, P(n)$ simply by executing all halting programs of length less than or equal to $|T|+c$, and running $T$ on their output.  If $T$ outputs "True" for these finitely many numbers, then $P$ is true.
Of course, the Halting problem places limits on the power of this method.
Essentially, this question boils down to:  What is the most succinctly stateable open conjecture?
EDIT:  By the way, an amazing implication of the argument I give is that to prove any theorem about the natural numbers, it suffices to prove it for finitely many values (those with low Kolmogorov complexity).  However, because of the Halting problem it is impossible to know which values!  If anyone knows a reference for this sort of thing I would also appreciate that.
 A: Regarding to prove any theorem about the natural numbers, it suffices to prove it for finitely many values ... impossible to know which values (where the context explains that the theorem is a universally quantified statement $\forall n\,P(n)$): this is trivial, and one value suffices. Namely, define $n_0$ as follows: if the statement is false, let $n_0$ be the smallest counterexample, otherwise let $n_0:=0$. Then the statement holds if and only if $P(n_0)$. 
A: It's quite possible that the Collatz conjecture provides an answer. Apply this function repeatedly. The conjecture is that this process will eventually reach the number 1, regardless of which positive integer is chosen initially. 

Not sure how many lines of code this would be. Probably 2 in Haskell.
A: Readers might be interested to know that congruential iterations similar to the Collatz 3n+1 problem were discovered "in the wild" while trying to understand the behavior of various busy beaver candidate machines. Since John Conway has shown that deciding termination of certain classes of such congruential iterations is undecidable, it may be the the boundary of undecidability already lies in one of these open busy beaver congruential iteration problems. For much further discussion and references see my old post on
sci.math, 13 Feb 1996, halting is weak?
http://groups.google.com/group/comp.lang.scheme/msg/b8c43aee2bc12241
http://google.com/groups?selm=WGD.96Feb13081831%40berne.ai.mit.edu
A: There is a 5-state, 2-symbol Turing machine for which it is not known whether it halts. See 
http://en.wikipedia.org/wiki/Busy_beaver.
A: The answer depends utterly and completely on the description language. Rogers called a description language "acceptable" if there is a pair of effective methods, one to convert standard programs to programs in the language D, and one to convert programs in D to standard programs.  (More precisely, these description languages are just numberings of the set of partial computable functions.) Now for any program whatsoever, there is an acceptable description language which assigns that program to index 0.  So any program you like can be the shortest example, if you pick the right acceptable numbering.  
This is the same kind of reason that, for any string of length 2 or more, there is a universal prefix-free machine that makes the string Kolmogorov random, and another universal prefix-free machine that makes the string not Kolmogorov random.  
A: May I suggest the use of Binary Lambda Calculus [1] for writing programs and measuring their size in bits?
There are many BLC programs of only a few dozen bits, comparable in complexity to 5 state TMs that need nearly 50 bits to describe, whose halting behavior is unknown.
Beyond that, there are programs like this 215 bit one for computing Laver tables [2], whose halting behavior is related to existence of large cardinals. A counterexample to Goldbach's conjecture can be found with a 267 bit program.
I decided to pose a question on mathoverflow [3] addressing the specific form of the question.
[1] https://tromp.github.io/cl/Binary_lambda_calculus.html
[2] https://codegolf.stackexchange.com/questions/79620/laver-table-computations-and-an-algorithm-that-is-not-known-to-terminate-in-zfc
[3] What's the smallest lambda calculus term not known to have a normal form?
A: You may find my blog post "Are small sentences of Peano arithmetic decidable?" relevant. In summary, John Langford and I investigated short sentences of Peano arithmetic. We enumerated them all (actually, our laptops did) and eliminated those that could be recognized as decidable. It quickly turned out that Diophantine equations were difficult to recognize as decidable. Among those we found two that gave a professional number theorist something to munch on (all quantifiers range over $\mathbb{N}$):
$$\exists a, b, c . \; a^2 - 2 = (a + b) b c$$
and
$$\exists a, b, c . \; a^2 + a - 1 = (a + b) b c.$$
The shortest unsolved sentence I am aware of is ($S$ is the successor function)
$$\forall a \exists b \forall c, d . \; (a+b)(a+b) \neq S(S( (S(S c)) \cdot (S(S d)))).$$
It says (more or less) that there are infinitely many primes of the form $x^2 - 2$.
What I found most surprising was that mixed quantifiers were easier than just straight universal or existential statements. It seems that with very few symbols to spare for the matrix, you cannot produce an interesting mixed-quantifier sentence.
A: This doesn't qualify as "shortest" but is my favorite example of why humans can't solve the halting problem:

for all odd numbers $n = 1,3,5,...$
    if $n$ is perfect, halt.

This program halts if and only if there is an odd perfect number. Of course, the query "is $n$ perfect" is not terribly short (but can be computed by adding one more for loop).
A: this question is apparently closely related to Wolframs research program of determining whether "small" Cellular Automata [CAs][1] are Turing Complete. if the CA is proved Turing Complete then by mapping with Turings halting problem, there exists an input for which termination of the CA cannot be proven. but also determining whether the CA is Turing complete can be very difficult and there are several so-far-indeterminate cases. a case where it succeeded but with a very complex proof is [2], some further details of the dynamics in [4]. see also [5] for a writeup of an ambitious somewhat recent "major attack" on the busy beaver problem that superseded many prior results. and there is also a related long tradition of research for finding small state universal TMs[3,6] probably dating to the ~1960s including results by Marvin Minsky. re Collatz conjecture candidate & a boundary with "nearby" problems similar to Conway-type, see also [7]
[1] Elementary cellular automata, wikipedia
[2] Rule 110, wikipedia
[3] tcs.se, whats the simplest noncontroversial 2 state universal TM
[4] tcs.se initial conditions for rule 110
[5] New-Millenium Attack on the Busy Beaver Problem by Ross et al
[6] The complexity of small universal Turing
machines: a survey Woods & Neary
[7] tcs.se, whats the nearest problem to the Collatz conjecture thats been successfully resolved?
A: The following is based on Waring's Problem:
For all n  floor((3/2)^n) + 3^n mod 2^n < 2^n. Kubina has tested this up to 471,600,000.
x = 9;
for( y = 4 ; x/y + x%y < y ; y *= 2 )
   x *= 3;
Assume that x and y are int's with unlimited size.
Whereas small Turing machines have been exhaustively analysed and, as Richard notes, there is a 5-state 2-symbol TM whose halting is unknown, I have not seen a similar analysis for other models of computation (Register Machines, LOOP programs, C programs). So I propose the above C  program (containing 32 symbols) as the shortest whose halting is unknown.
In the program x contains powers of 3 and y contains corresponding powers of 2 (x*=3 multiplies x by 3).
