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
    • ReedSolomonReedMuller: Reed-Solomon codes (univariate polynomial evaluation over GF(2ᵏ), injectivity and minimum-distance bounds, computed GF(8) demonstration) and Reed-Muller codes (multivariate polynomial evaluation on the boolean hypercube, with RM(1,2) example)
  • 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
    • Multiplicity: multiplicity of a root, the degree budget counted with multiplicity, the derivative test for repeated roots, and the characteristic-2 collapse (X − 1)²ʳ = X²ʳ − 1
    • Ideals: ideals, kernels, quotients, and the prime/maximal hierarchy
    • Multilinear: multivariate polynomials, the multivariate Schwartz–Zippel bound, and the multilinear extension (MLE) of boolean functions over 𝔽₂
  • Field
    • Galois: finite fields GF(pⁿ) and their structure
    • Characteristic: the characteristic of a field; why it is prime, char-2 facts (x = −x, translation involutions), the freshman's dream, and the squaring dichotomy (2-to-1 odd vs 1-to-1 char 2)
    • 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
    • BinaryFields: GF(2) and GF(2ⁿ), boolean gates as polynomials, Freshman's dream, Frobenius, and trace map
    • G8: GF(8) hand-rolled as bit triples with schoolbook multiplication, so worked examples can evaluate with decide
• 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
  • Merkle: binary hash trees and authentication paths; honest paths verify, plus a concrete tree over GF(8) showing a nonlinear hash is binding where a+b is not
  • ZK
    • Schnorr: sigma protocol for knowledge of a discrete log; completeness, special soundness, and honest-verifier zero-knowledge
    • Sumcheck: the sumcheck protocol on the boolean hypercube; the soundness per round is read off the multivariate Schwartz–Zippel bound
    • BinaryFRI: proximity testing over binary fields; additive folding via q(x) = x² + β·x, the fold chain, and the Reed-Solomon distance properties behind the proximity question
    • Binius: the full binary-field argument for a boolean circuit, end to end on an AND gate; MLE → sumcheck → binary FRI → Merkle, with the soundness budget
• Examples: end-to-end runs that wire the pieces above together
  • Sumcheck: a sumcheck run over ℤ/7ℤ with a quadratic round polynomial, where two values cannot serve as the message and the challenges land outside the interpolation nodes
  • BinaryFRI: a binary FRI micro-run over GF(8) (Algebra/Field/G8.lean); a real RS [8, 4, 5] codeword of a message polynomial and two fold rounds down to a constant, with the verifier's fiber checks at each round

Build

lake build

The Mathlib revision is pinned in lakefile.toml.