Intro

This project formalizes fundamental worst-case-to-average-case reductions in lattice-based cryptography using Lean4. Along the way, we aim to build a library of formalized mathematical tools for verifying future lattice-based algorithms.

LLM Usage

All definitions and theorem statements are written by humans, but most proofs are generated by LLMs. As a result, some Lean proofs may look more complicated than necessary; this usually means they were “vibe‑proved” by an LLM. What matters is the statement of each theorem. As long as the statement is correct, we are good.

LLMs used in this project include GPT-5.2-Codex, Claude Sonnet 4.5, and Aristotle from Harmonic. We also credit the lean-lsp-mcp project, which is the key tool enabling agentic proof generation.

Using LatticeCrypto library in your project

To add LatticeCrypto as a dependency to your Lean project, add the following to your lakefile.toml:

[[require]]
name = "LatticeCrypto"
scope = "xyguo"
rev = "main"

Project Outline

Phase 1: Mathematical Foundations

1.1 Basic Lattice Theory

• Module: LatticeCrypto.Foundations.Lattice
• Lattice definition and properties
• Basis representation and linear independence
• Lattice operations (shift, scaling)
• Related structures (coset, dual lattice)
• Fundamental lattice parameters (fundamental domain, determinant)
• Successive minima and Minkowski’s First and Second Theorems

1.2 Major analytic tools

• Module: LatticeCrypto.Foundations.Lattice
• Discrete Gaussian
  • Probability: common distributions, expectation, concentration inequalities (Markov/Chebyshev/Chernoff)
  • Fourier transform, FFT, Poisson's Summation Formula
• Banasczyk's transference theorem
• Smoothing parameter

1.3 Lattice Algorithms

• Module: LatticeCrypto.Foundations.Algorithms
• Gram-Schmidt orthogonalization (using Mathlib version)
• The LLL (Lenstra-Lenstra-Lovász) basis reduction algorithm
• Babai's Nearest Plane algorithm
• Discrete Gaussian sampling
• The BKZ (Block Korkine-Zolotarev) algorithm

1.4 Lattice Problems and Hardness

• Module: LatticeCrypto.Foundations.Hardness
• Computational complexity: asymptotics, reductions, query complexity
• Definition of hard lattice problems (SVP, CVP, GapSVP, GapCVP, SIVP)
• Reduction between problems (?)
• Formal statements of hardness assumptions (?)

Phase 2: Cryptographic Primitives

2.1 Short Integer Solution (SIS)

• Module: LatticeCrypto.Primitives.SIS
• SIS problem definition
• CRHF from SIS

2.2 Learning With Errors (LWE)

• Module: LatticeCrypto.Primitives.LWE
• LWE problem definition and variants
• Error distribution (discrete Gaussian)
• PKE from LWE

2.3 Ring/Module-SIS and Ring/Module-LWE

• Module: LatticeCrypto.Primitives.RingLWE, LatticeCrypto.Primitives.ModuleLWE, LatticeCrypto.Primitives.RingSIS, LatticeCrypto.Primitives.ModuleSIS
• Polynomial rings and ideals
• Ring-LWE/SIS problem definition
• Module-LWE/SIS generalization

Phase 3: Worst-case to Average-case Reductions

3.1 SIS ([Micciancio-Regev03])

3.2 LWE ([Regev05])

3.3 Ring-LWE/SIS ([LPR12])

3.4 Module-LWE/SIS ([LS12])