Algebra & Cryptography

A collection of Lean 4 files written as a personal study of modern algebra and its applications to cryptography. Built on top of Mathlib.

Status: heavily work in progress. Expect gaps, rough edges, and frequent rewrites; files will be added, restructured, and refined over time as the study progresses.

Layout

• Algebra: core algebraic structures
  • Code
    • Hamming: the [7,4,3] Hamming code; generator and parity-check matrices, codewords, syndrome decoding, single-error correction, and a worked example
    • Hypergraph: hypergraph incidence matrix as a parity-check matrix, k-uniformity, minimum distance, unique syndrome decoding theorem, and the Hamming [7,4,3] code as a 4-uniform hypergraph
  • Group
    • Cyclic: cyclic groups and their connection to ℤ/nℤ
  • Ring
    • Polynomials: polynomial rings, working over 𝔽₃[X]
    • RootsInterpolation: the roots bound (Schwartz–Zippel), interpolation, and vanishing polynomials
    • Ideals: ideals, kernels, quotients, and the prime/maximal hierarchy
  • Field
    • Galois: finite fields GF(pⁿ) and their structure
    • QuadraticResidues: squares in 𝔽ₚ, Euler's criterion, and the Legendre symbol
    • RootsOfUnity: roots of unity in finite fields, primitive roots, and the connection to cyclic subgroups
• Crypto: cryptographic schemes built on the above
  • DiffieHellman: key exchange in a cyclic group
  • Rsa: RSA correctness from Bézout and Euler's theorem
  • EllipticCurves: Weierstrass curves over finite fields
  • Paillier: additively homomorphic encryption, decryption correctness proven as algebra
  • McEliece: code-based encryption; scrambling by S·G·P, decryption correctness from a decoder hypothesis, and a fully executable [7,4,3] Hamming code instance
  • ZK
    • Schnorr: sigma protocol for knowledge of a discrete log; completeness, special soundness, and honest-verifier zero-knowledge

Build

lake build

The Mathlib revision is pinned in lakefile.toml.