2023.08.18 16:29:04 (Mastodon 110911562980768637, Twitter 1692574232155398515) from Daniel J. Bernstein:
Just uploaded new version of my paper "Understanding binary-Goppa decoding": https://cr.yp.to/papers.html#goppadecoding Includes detailed comparisons of all ten theorems to formalizations of the theorems in HOL Light and in Lean. Also explains how to run HOL Light and Lean to verify the proofs.