[FOM] Prove something weaker!

[Timothy Y. Chow]

Joe Shipman wrote:
> I'm interested in the phenomenon of famous conjectures being stated in 
> strong forms when even very much weaker forms of them are unproven.
>
> For example, I don't understand why I see a lot more talk about the 
> inability to prove that P is not NP, when the inability to prove that P 
> is not PSPACE seems far more surprising.

Isn't this obvious?  The usual role of "big" conjectures is to outline 
what we think should be true, not to demarcate the boundaries of what we 
can currently prove.  The latter task is primarily of interest to the 
experts who are in the trenches trying to push forward the boundary 
incrementally.  (Though once in a while, non-specialists do get into the 
mood of chuckling at how incompetent we all are at the proving business, 
in which case the weakest possible conjecture provides the most 
amusement.)

> Can anyone supply a technical reason that separating P and PSPACE 
> shouldn't be easier to tackle than separating P from NP?

Surely not.  But why stop at P vs. PSPACE?  Why not ask to show that NEXP 
is not contained in P/poly, or that NP has superlinear circuit lower 
bounds?  That'll get you closer to the current frontier.  Ryan Williams 
showed in 2010 that NEXP (in fact, NTIME[2^n]) does not have polysize ACC 
circuits.

> I'm also interested in collecting other examples of well-known 
> conjectures for which there are much weaker versions that seem almost 
> equally difficult to make progress on, besides the two examples above.

I would think that most conjectures fall into this category, but if you 
want examples where the gap between what we can prove and what we 
conjecture to be true is especially large, then Schanuel's conjecture 
comes to mind.  So does the entire Langlands program.

Tim