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
  • Group
    • Cyclic: cyclic groups and their connection to ℤ/nℤ
  • Ring
    • Polynomials: polynomial rings, working over 𝔽₃[X]
    • 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
• 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

Build

lake build

The Mathlib revision is pinned in lakefile.toml.