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. A library whose subject is a Mathlib-facing tactic, such as hex-rcf, has no computational half and appears only in the Mathlib column.

Component	Computational	Mathlib layer
Foundations	HexBasic	n/a
Exact word arithmetic	HexArith	n/a
Certified primality	HexPrimality	HexPrimalityMathlib
Dense univariate polynomials	HexPoly	HexPolyMathlib
Sparse multivariate polynomials	HexMvPoly	HexMvPolyMathlib
Modular arithmetic	HexModArith	HexModArithMathlib
Polynomials over a prime field	HexPolyFp	HexPolyFpMathlib
Sparse univariate polynomials	HexSparsePoly	HexSparsePolyMathlib
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
Conway polynomials	HexConway	n/a
Finite fields F_p[x]/(f)	HexGFqField	n/a
Packed GF(2) polynomials	HexGF2	HexGF2Mathlib
Canonical finite fields	HexGFq	HexGFqMathlib
Determinants	HexDeterminant	HexDeterminantMathlib
Bareiss determinant	HexBareiss	HexBareissMathlib
Gram-Schmidt	HexGramSchmidt	HexGramSchmidtMathlib
LLL lattice reduction	HexLLL	HexLLLMathlib
Integer polynomial factorization	HexBerlekampZassenhaus	HexBerlekampZassenhausMathlib
Graph canonical labelling	HexGraphIso	HexGraphIsoMathlib
Resultants and discriminants	HexResultant	HexResultantMathlib
Algebraic numbers	HexNumberField	HexNumberFieldMathlib
Number field towers	HexNumberFieldTower	HexNumberFieldTowerMathlib
Real-closed-field decision (rcf tactic)	n/a	HexRCF

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.