verifying-crypto-with-lean/lean-toolchain at main - saymrwulf/verifying-crypto-with-lean - Forgejo: Beyond coding. We forge.

saymrwulf/verifying-crypto-with-lean

mirror of https://github.com/saymrwulf/verifying-crypto-with-lean.git synced 2026-07-17 18:40:45 +00:00

saymrwulf 45048d4898 Verifying Cryptography with Lean 4: complete 12-chapter curriculum

- 53-page LaTeX/TikZ book (main.pdf + full sources): from zero background
  to reading the real Ed25519/Pasta verification projects
- runnable exercises with sorry-holes + complete solutions for chapters
  2-7, 9, 12; every solution file compiles clean (zero errors, no sorry)
  against Lean v4.30.0-rc2 + Mathlib 5450b53e
- lake project pinned to the same toolchain/Mathlib the solutions were
  verified with; students fetch the Mathlib cache, never build it
- honesty ledger in README: what was machine-checked and how

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

2026-07-03 09:44:40 +02:00

1 line

29 B

Text

Raw Permalink Blame History

leanprover/lean4:v4.30.0-rc2