saymrwulf/verifying-crypto-with-lean
1
0
Fork 0
mirror of https://github.com/saymrwulf/verifying-crypto-with-lean.git synced 2026-07-16 18:32:02 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
verifying-crypto-with-lean/exercises
History
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
..
Ch02.lean Verifying Cryptography with Lean 4: complete 12-chapter curriculum 2026-07-03 09:44:40 +02:00
Ch03.lean Verifying Cryptography with Lean 4: complete 12-chapter curriculum 2026-07-03 09:44:40 +02:00
Ch04.lean Verifying Cryptography with Lean 4: complete 12-chapter curriculum 2026-07-03 09:44:40 +02:00
Ch05.lean Verifying Cryptography with Lean 4: complete 12-chapter curriculum 2026-07-03 09:44:40 +02:00
Ch06.lean Verifying Cryptography with Lean 4: complete 12-chapter curriculum 2026-07-03 09:44:40 +02:00
Ch07.lean Verifying Cryptography with Lean 4: complete 12-chapter curriculum 2026-07-03 09:44:40 +02:00
Ch09.lean Verifying Cryptography with Lean 4: complete 12-chapter curriculum 2026-07-03 09:44:40 +02:00
Ch12.lean Verifying Cryptography with Lean 4: complete 12-chapter curriculum 2026-07-03 09:44:40 +02:00