Please excuse me if this is a basic question, or badly phrased, I'm very new to mathematics in general.
In Fermat's factorization method - based on the fact that every odd number can be expressed as n = x^2 - y^2 is there any formal proof that x and y cannot be derived quickly without resorting to any type of trial and error?
I'm aware of other factorizations methods such as the quadratic sieve but don't understand fully how they work yet.
There are (basically) no non-trivial lower bounds on any interesting algorithmic problem other than in restricted models. In particular, it is not known that factoring is not easy (i.e. in P), though it is certainly suspected by most researchers in the area that factoring is not easy.
As an aside, Fermat's factorization "method" isn't really a method unless you specify how you come up with the pairs $x,y$, and when you do you find out that it's a pretty bad factoring method.