Using Mathlib | Cryptography Academy

What Is Mathlib?

Mathlib is a community-maintained library containing thousands of mathematical definitions and theorems. For cryptography, we rely heavily on its algebraic structures: groups, rings, and fields.

Why Mathlib matters: Instead of defining groups from scratch, we use Mathlib's battle-tested definitions. This gives us access to thousands of proven lemmas for free.

Algebraic Structures

Mathlib organizes algebra using typeclasses. Here are the key structures for cryptography:

Group

A set with an associative operation, identity, and inverses. Cryptographic groups (elliptic curves, multiplicative groups) are modeled this way.

-- G is a group means we have:
-- * : G → G → G      (multiplication)
-- 1 : G              (identity)
-- ⁻¹ : G → G         (inverse)

variable [Group G]

-- These theorems are available:
#check @mul_assoc G _        -- (a * b) * c = a * (b * c)
#check @one_mul G _          -- 1 * a = a
#check @inv_mul_cancel G _   -- a⁻¹ * a = 1

CommGroup

A commutative (abelian) group. Most cryptographic groups are commutative.

variable [CommGroup G]

#check @mul_comm G _   -- a * b = b * a

Ring and Field

Rings have addition and multiplication. Fields additionally have division (multiplicative inverses for nonzero elements).

variable [Field F]

-- We get both additive and multiplicative structure:
#check @add_comm F _        -- a + b = b + a
#check @mul_add F _         -- a * (b + c) = a*b + a*c
#check @mul_inv_cancel F _  -- a ≠ 0 → a * a⁻¹ = 1

ZMod n

Integers modulo n. When n is prime, ZMod n is a field.

-- Arithmetic in ZMod works as expected
example : (3 : ZMod 7) + 5 = 1 := rfl  -- 3 + 5 = 8 ≡ 1 (mod 7)

Type Classes in Action

The bracket notation [Group G] means "G has a Group structure." Lean finds the right instance automatically:

-- A theorem that works for ANY group
theorem my_inv_inv [Group G] (a : G) : a⁻¹⁻¹ = a := by
  -- Mathlib already has this!
  exact inv_inv a

The power of polymorphism: prove once, use for any group.

Finding Theorems

Mathlib has thousands of lemmas. Here's how to find them:

Naming conventions

Lemma names describe what they do: mul_comm (multiplication commutes), add_assoc (addition associates), inv_mul_cancel (inverse times element is identity).

exact?

The exact? tactic searches for a lemma that closes the current goal:

example [Group G] (a b : G) : a * b * b⁻¹ = a := by
  exact?  -- suggests: exact mul_inv_cancel_right a b

Online documentation

Browse the Mathlib4 docs to explore available definitions and theorems.

Cryptographic Example

Here's how Mathlib structures appear in cryptographic code:

-- A Schnorr-like discrete log setting
structure DLSetting where
  G : Type*              -- The group
  [grp : CommGroup G]     -- It's a commutative group
  g : G                   -- Generator
  q : ℕ                   -- Order of g
  g_order : g ^ q = 1      -- g^q = identity

-- With this structure, we inherit all group lemmas:
example (s : DLSetting) : s.g * s.g⁻¹ = 1 := by
  exact mul_inv_cancel s.g

The [grp : CommGroup G] annotation makes G a commutative group, giving us access to all of Mathlib's group theory.

Common Mathlib Imports

You'll often see these imports in cryptographic code:

import Mathlib.Algebra.Group.Basic       -- Group theory
import Mathlib.Algebra.Field.Basic       -- Field theory
import Mathlib.Data.ZMod.Basic           -- Integers mod n
import Mathlib.NumberTheory.Divisors     -- Divisibility
import Mathlib.Data.Polynomial.Basic    -- Polynomials

Next Steps

You now understand how Mathlib provides algebraic foundations. Next, learn the patterns specific to cryptographic formalizations:

Next: Cryptographic Patterns →