2023.03.17 15:40:37 (Mastodon 110039376681280275, Twitter 1636754337128144896) from Daniel J. Bernstein:
Major update of "Multi-ciphertext security degradation for lattices" paper: https://cr.yp.to/papers/lprrr-20230317.pdf Main optimization is integrated into the central theorem statement, backed by a proof (https://cr.yp.to/2023/lprrr-20230317.ml) verified by the HOL Light theorem prover (https://www.cl.cam.ac.uk/~jrh13/hol-light/).