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"

The requirement installs the libraries in the table below at a single coherent pinned set. The generated import Hex umbrella re-exports every aggregated library:

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

Component	Computational	Theory
Foundations	HexBasic	n/a
Fixed-precision power series	HexTruncatedSeries	HexTruncatedSeriesTheory
Exact word arithmetic	HexArith	n/a
CRT and rational reconstruction	HexModular	n/a
Certified primality	HexPrimality	HexPrimalityTheory
Bounded elliptic-curve certificates	HexECPP	HexECPPTheory
Dense univariate polynomials	HexPoly	HexPolyTheory
Fast dense-polynomial algorithms	HexPolyFast	n/a
Modular arithmetic	HexModArith	HexModArithTheory
Sparse multivariate polynomials	HexMvPoly	HexMvPolyTheory
Matrices	HexMatrix	HexMatrixTheory
Polynomials over a prime field	HexPolyFp	HexPolyFpTheory
Sparse univariate polynomials	HexSparsePoly	HexSparsePolyTheory
Integer polynomials	HexPolyZ	HexPolyZTheory
Quotient rings F_p[x]/(f)	HexGFqRing	n/a
Hensel lifting	HexHensel	HexHenselTheory
Complex root isolation	HexRoots	HexRootsTheory
Real root isolation	HexRealRoots	HexRealRootsTheory
Row reduction	HexRowReduce	HexRowReduceTheory
Finite-field factorization	HexBerlekamp	HexBerlekampTheory
Conway polynomials	HexConway	n/a
Finite fields F_p[x]/(f)	HexGFqField	n/a
Packed GF(2) polynomials	HexGF2	HexGF2Theory
Canonical finite fields	HexGFq	HexGFqTheory
Determinants	HexDeterminant	HexDeterminantTheory
Bareiss determinant	HexBareiss	HexBareissTheory
Gram-Schmidt	HexGramSchmidt	HexGramSchmidtTheory
LLL lattice reduction	HexLLL	HexLLLTheory
Integer polynomial factorization	HexBerlekampZassenhaus	HexBerlekampZassenhausTheory
Permutation groups	HexPermGroup	HexPermGroupTheory
Graph canonical labelling	HexGraphIso	HexGraphIsoTheory
Resultants and discriminants	HexResultant	HexResultantTheory
Algebraic numbers	HexNumberField	HexNumberFieldTheory
Number field towers	HexNumberFieldTower	HexNumberFieldTowerTheory
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
• Graph canonical labelling (HexGraphIso): blog post, Zulip
• Algebraic numbers (HexNumberField): blog post, Zulip, LinkedIn

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