Implementing Cryptographic Primitives in Lean 4
In this talk I will describe the experience of using Lean 4 as a fully-fledged programming language to implement various number theoretic primitives used in cryptography. In particular, we will go through the examples of efficient implementations of finite field arithmetic, fast elliptic curve group operations, and some commonly used cryptographic hash functions.
Along the way I plan on reflecting on the lessons learned in building structurally and mathematically complex libraries in Lean 4. I will also cover some future directions and long-term visions of Lean 4's place in modern cryptography.