How should I express theorems without a proof in a research paper? What do you do when you have a conjecture, and you run experiments that confirm your conjecture, but you are unable to provide a formal proof (perhaps because it's too complicated)? Do you name them as conjectures or observations or... what?

This is in the context of a CS theory paper.
In mathematics and TCS (which is really a branch of mathematics), if you don't have a proof, you don't have a theorem.  (You write "experiments", which I will assume means "computer calculations".  Please let me know if this is not the case.)  Doing some computer calculations can be interesting and even sometimes publishable, but it does not constitute any kind of proof, formal or otherwise.  (Added: Well, unless it does, of course.  You can prove a theorem by reducing it to a finite calculation and doing that calculation by hand or by computer or some of both.  You can't prove a theorem which pertains to infinitely many cases by doing finitely many of them and claiming "and so on".) Also, although the word "confirm" is often used in this way in empirical science, in mathematics to "confirm a conjecture" means to prove it.  

I see two possible questions here:


How do I write up computational evidence for a result that I cannot prove in a paper?   
Can I publish a paper in which I do not prove my conjecture but only have computational evidence towards it?


The first question is more straightforward.  You state the conjecture -- i.e., the statement that you think is a theorem but can't yet prove.  Some discussion of the provenance of the conjecture is probably a good idea but is not strictly necessary.  However, if you got the conjecture from somewhere else you must indicate that.  Then you document the calculations you made.  Finally, you probably want to make some remarks about why the calculations make you confident in your conjecture (if that is the case).  Here sometimes informal reasoning can be helpful: e.g. if your conjecture is that for two sequences of integers a_n and b_n that a_n and b_n are always congruent modulo 691, then if you check this for the first 100,000 terms then in some naive sense the probability that this happened by accident is (1/691)^{100,000}, which is vanishingly small.

The second question is much more complicated.  It can be hard to publish papers in which you do not prove a theorem but "only" give computer evidence...but not as hard as it used to be.  Mathematics is slowly becoming more enlightened about the merits of computer calculations.  I would say though that you need to understand the field much better to be able to predict whether a paper primarily containing computations would be publishable than to publish a more "theoretical" paper: many, many referees and journals will say "no theorem, no proof, no paper", so you should expect to work much harder to sell your work.