[London Learning Lean] Post-quantum cryptography, by Wrenna Robson.

London Learning Lean is a seminar where mathematicians discuss more advanced mathematical formalisations (i.e. typically beyond undergraduate level) in the Lean theorem prover.