2024.04.16 15:47:30 (Mastodon 112281678665634187, Twitter 1780261762262241781) from Daniel J. Bernstein:
https://cr.yp.to/papers.html#latticeasymp has (1) an asymptotic thm; (2) proof; (3) formally verified proof. Had originally included #1+#3 in https://cr.yp.to/papers.html#lprrr. Later realized that #2 still has value: gives idea of #3; illustrates proof size that's formally verifiable in a few person-weeks.