Quantum algorithms for LWE

Stream: maths

[Wrenna Robson]

Is anyone looking into verifying key components of this paper? https://eprint.iacr.org/2024/555.pdf

For context: this is a recent preprint that claims an effective polynomial-time quantum algorithm for solving the "learning with errors" problem.

[Frédéric Dupuis]

I think step one is to wait a bit for people to actually read the paper! There's already an erratum on the author's website after it was pointed out that there is an impossible choice of parameters going on in the paper.

[Wrenna Robson]

That is fair! Mainly I was wondering what role verification systems can have at this sort of early stage when everyone is wondering "does this work".

[Frédéric Dupuis]

Right now I would say it's just too early. Formalization would start to make sense when we reach the stage "looks pretty solid, but there's still some lingering doubt".

[Wrenna Robson]

Fair :)

[Frédéric Dupuis]

...and now it turns out there's a bug in the paper that the author doesn't know how to fix.

[Gareth Ma]

Even if it’s correct, I don’t think Lean has any/much cryptography yet?

[Shreyas Srinivas]

This is a result which also requires algorithms and complexity

[Wrenna Robson]

I wouldn't say it's necessarily a result about cryptography so much as one with cryptographic consequence.

[Frédéric Dupuis]

Right, formalizing this wouldn't really require much background in cryptography per se.

[Wrenna Robson]

Though it would require reasoning about quantum algorithms, which Lean is also not equipped for yet I think.

[Frédéric Dupuis]

True, but that's not really crypto :-) Ironically, it might actually be the case that the hardest part would be formalizing the fact that the classical parts of the algorithm run in polynomial time.

[Shreyas Srinivas]

Lean is not equipped for reasoning with algorithms.

[Shreyas Srinivas]

To be fair the LWE result was a godel prize winner. So it would be a non-trivial breakthrough if this paper could be formalised, even if only to identify the errors. The effort-reward tradeoff is more even on this one