Which post-quantum cryptosystems are more efficient than RSA?
I did not claim that they outperform RSA in particular and I would not call RSA a state of the art public key cryptosystem. Actually, I would strongly suggest against using RSA without first having a deep dive into the field of number theory. However, for extreme RSA key sizes (e.g. 4096 bit) NewHope does actually outperform RSA and definitely outperforms some ECC counterparts.
NewHope has not been proven to be quantum resistant. I think researchers generally believe that NewHope will be proven to be quantum resistant, but there is the problem of adapting Micciancio's regular lattice proof to ideal lattices.
That’s right, it hasn’t. Just as almost every other candidate in the NIST competition. However, none of the currently employed public key crypto systems has even been proven to be secure against standard computers and they can definitely be broken by a (powerful) quantum computer. So I would still favor taking a scheme that most likely is secure against quantum computing over one that can definitely be broken by it, especially if their performance does not differ too much anymore.
Nothing can be "proven" to be quantum resistant. Even if we can show a tight reduction to LWE, and we believe that LWE is efficiently solvable (let's say LWE is not in BQP), it is still possible that the cryptosystem at the given parameters is broken. In the classical case, it doesn't matter whether or not the RSA problem is "hard" (more formally, the RSA problem is not in BPP), it matters if the RSA4096 problem has an efficient solution for many real world instances. So, yeah, the talk of "proving" security---while interesting---isn't very useful.
>However, for extreme RSA key sizes (e.g. 4096 bit) NewHope does actually outperform RSA.
Yep, it's definitely a scaling thing. If it weren't then we could simply use Daniel Bernstein's (et al) proposal for Post Quantum RSA.