The microblog: 2023.07.26 13:46:28

2023.07.26 13:46:28 (Mastodon 110780690497105946, Twitter 1684198514543165441, Nitter 1684198514543165441) from Daniel J. Bernstein:

Formally verified theorems about decoding Goppa codes: This is using the Lean theorem prover; I'll try formalizing the same theorems in HOL Light for comparison. This is a step towards full verification of fast software for the McEliece cryptosystem.