2022.02.18 08:14:45 (1494571069839065088) from Daniel J. Bernstein:
No. Lattice KEMs under consideration for deployment (NTRU, Kyber, Frodo, etc.) do _not_ have NP-hardness proofs. (There's also no serious hope of crossing the dividing lines.) Questions to ask: Where did the pervasive misinformation on this topic originate? Who benefits from it?