Have quantum computers been proven to speed up any matter modeling algorithm?

Personally, I think quantum chemistry is one of the most promising applications for quantum computers because the problem itself is fundamentally quantum, so there is an obvious argument why we should expect a quantum speedup.

Are there matter modeling algorithms for quantum computers with proven quantum speedup?

Here by 'proven,' I just mean that it has been mathematically demonstrated, not that they have necessarily been implemented on a practical device.

I would be especially interested in algorithms that could integrate directly into existing ab initio methods.

FCI (Full Configuration Interaction)

The FCI expansion of a wavefunction allows us to obtain the exact energy of a system given a basis set with $$N$$ spatial orbitals. On a classical computer, for a singlet state with no spatial symmetry, if we have $$N$$ spatial orbitals and $$k$$ pairs of electrons, then we have $${N \choose k}^2$$ Slater determinants in the FCI expansion of a wavefunction, and therefore $${N \choose k}^2$$ parameters to optimize if we want to get the energy.

Since $${N \choose k}^2$$ is a multi-variable function, and isn't expressed explicitly as an "exponential" or "polynomial" in either of the two variables, I like to use the first set of inequalities in the "Bounds and asymptotic formulas" section of this page (my expressions below are the same, but with the square that I mentioned in my first paragraph):

$$\tag{1} \frac{N^{2k}}{k^{2k}} \le {N \choose k}^2 \le \frac{N^{2k}}{(k!)^2}.$$

For 10 electrons (one H2O molecular has 10 electrons, for example) we have $$k=5$$ pairs of electrons, so my Eq. 1 becomes the following:

$$\tag{2} \frac{1}{9765625}N^{10} \le {N \choose 5}^2 \le \frac{1}{14400}N^{10}.$$

Although the denominator 9765625 looks large, since $$N$$ is usually at least double the size of $$k$$, we can see that the number of parameters that we have to optimize, which is $${N \choose 5}^2$$, is growing like a degree-10 polynomial of $$N$$, divided by a comparatively small factor. This means that as we want more and more accurate energies (via basis sets with more and more orbitals), the computational cost grows tremendously.

Most systems of interest have far more than 10 electrons, and the above argument becomes stronger and stronger as we raise the number of pairs (denoted by $$k$$) of electrons. This is also explained in answers to: What are the limitations of FCI?

What can quantum computers do?

Table 1 of this paper shows that the space complexity (equivalent to the number of parameters that needed to be optimized in the above-described classical algorithm) on a quantum computer is linear with respect to the number of orbitals:

Are we sure?

Just as we haven't proven whether or not P=NP, we also haven't proven whether or not NP = QMA, and many other things (see this answer of mine on QCSE). So when you say that "proven" means "mathematically demonstrated", I want to emphasize that there is no "mathematical" proof that classical computers can't also do the above computation with O(N) complexity, but I think it's fair to say that it has been mathematically proven that quantum algorithms in the above table have a smaller quantum space complexity than the classical space complexity of the best known classical FCI algorithms.

Finally, one thing about which I wish more quantum computing researchers were to be more honest, is the difference between "quantum space complexity" and "classical space complexity". Right now I would rather have an algorithm that requires $$2^N$$ classical bits than one that requires $$N^2$$ qubits, and so would anyone that understands that even $$10^2$$ qubits is less accessible than $$2^{10}=1024$$ classical bits. I know that you touched on the difference between "mathematically demonstrated" vs "physically demonstrated", but there is actually a mathematical difference in the power of a qubit vs a classical it, and there's also a mathematical difference in how hard they are to make: This touches on my notion of "engineering complexity" which I mentioned in my answer to this QCSE question.

VQE (Variational Quantum Eigensolver)

Since VQE is a hybrid algorithm that evaluates energy approximations on quantum computers and optimizes anstaz parameters on a classical computer, and since the number of ansatz parameters to optimize in FCI scales according to what I wrote in the first section in this answer, VQE does not seem to provide any advantage over classical computers for FCI. It has been discussed for other ansatze such as a "unitary coupled cluster" ansatz, but the benefits of using unitary coupled cluster ansatze (if any) over more tractable methods, are not as clear as the benefits of FCI over more tractable methods.

Conclusions

• Quantum computers can do FCI with O(N) quantum space complexity, for N orbitals. The best known classical algorithms for FCI scale much more severely.
• Quantum space complexity and classical space complexity are not the same thing, so we cannot fairly compare them "mathematically".
• When we say that quantum computers can do FCI more efficiently than classical computers (assuming no difference between quantum computational complexity and classical computational complexity), VQE is not the algorithm in mind. VQE is a hybrid quantum/classical algorithm, and for FCI the classical part has the same asymptotic computational complexity as solving the FCI problem entirely on a classical computer would have.