hex

Verified computational algebra in Lean 4: an aggregator for the released hex libraries.

• Manual: https://kim-em.github.io/hex-dev/
• API documentation: https://leanprover.github.io/hex/docs

Quickstart

Add to your lakefile.toml:

[[require]]
name = "hex"
git = "https://github.com/leanprover/hex.git"
rev = "main"

Then import Hex re-exports every library in the table below at a single coherent pinned set:

import Hex

open Hex

-- Exact, fraction-free integer determinant.
def M : Matrix Int 3 3 := #m[2, 1, 1; 1, 2, 1; 1, 1, 2]
#eval M.det   -- 4

-- LLL: reduce an integer lattice basis and read off a provably short vector.
-- The `by decide` arguments discharge the reduction-factor side conditions.
def L : Matrix Int 3 3 := #m[1, 1, 1; 1, 0, 2; 3, 5, 6]
#eval lllNative.firstShortVector L (3 / 4) (by decide +kernel) (by decide +kernel) (by decide)

To depend on just one piece, require that library directly (for example hex-lll for the Mathlib-free LLL core) instead of the aggregator.

Libraries

Each computational library is Mathlib-free; its Mathlib correspondence proofs and Mathlib-facing API, where they exist, live in a separate *-mathlib library.

Component	Computational	Mathlib layer
Foundations	HexBasic	n/a
Exact word arithmetic	HexArith	n/a
Dense univariate polynomials	HexPoly	HexPolyMathlib
Sparse multivariate polynomials	HexMvPoly	HexMvPolyMathlib
Modular arithmetic	HexModArith	HexModArithMathlib
Polynomials over a prime field	HexPolyFp	n/a
Integer polynomials	HexPolyZ	HexPolyZMathlib
Quotient rings F_p[x]/(f)	HexGFqRing	n/a
Hensel lifting	HexHensel	HexHenselMathlib
Complex root isolation	HexRoots	HexRootsMathlib
Real root isolation	HexRealRoots	HexRealRootsMathlib
Matrices	HexMatrix	HexMatrixMathlib
Row reduction	HexRowReduce	HexRowReduceMathlib
Finite-field factorization	HexBerlekamp	HexBerlekampMathlib
Determinants	HexDeterminant	HexDeterminantMathlib
Bareiss determinant	HexBareiss	HexBareissMathlib
Gram-Schmidt	HexGramSchmidt	HexGramSchmidtMathlib
LLL lattice reduction	HexLLL	HexLLLMathlib
Integer polynomial factorization	HexBerlekampZassenhaus	HexBerlekampZassenhausMathlib

Announcements

• LLL lattice reduction (HexLLL): blog post, Zulip, LinkedIn
• Integer polynomial factorization (HexBerlekampZassenhaus): blog post, Zulip, LinkedIn

Development of the full project (including unreleased libraries) happens in the hex-dev monorepo.