Post-quantum crypto

Stream: Lean for teaching

[Matthew Ballard]

I very much enjoyed teaching a math/cs course on cryptography in Fall 22. |

The programming component was in Go because that was a different time for Lean 4. I need to start thinking about teaching for Fall '24 and it is clear that Lean is mature enough to handle everything in that course. But a greater focus on post-quantum algorithms might better survive the test of time.

I haven't thought deeply about how to structure the course. If people have thoughts, please share.