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	—
Matrices	HexMatrix	HexMatrixMathlib
Row reduction	HexRowReduce	HexRowReduceMathlib
Determinants	HexDeterminant	HexDeterminantMathlib
Bareiss	HexBareiss	HexBareissMathlib
Gram-Schmidt	HexGramSchmidt	HexGramSchmidtMathlib
LLL	HexLLL	HexLLLMathlib

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