kim@lean:~$ cat posts/2026·09·08.md

Exact algebraic numbers and number fields in Lean

2026·09·08 [computer algebra] [lean]

I'm happy to announce the release of further packages for Hex, the computer algebra library for Lean, following lattice basis reduction, certified integer polynomial factorization and certified graph isomorphism.

Today we have exact algebraic numbers, and arithmetic and factorization in number fields.

Everything below is compiled as part of building this page, against the released v0.4.0; the Hex manual covers these libraries and the rest of Hex in full. To follow along, add to your lakefile.toml:

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

Algebraic numbers

An algebraic number is a root of an integer polynomial. You name one by giving an approximation, and the nearest root wins:

-- An algebraic number is a root of an integer polynomial, named by an
-- approximation: the nearest root wins.
def s2 : AlgebraicNumber := ZPoly.rootNear #p[-2, 0, 1] 1.4
def s3 : AlgebraicNumber := ZPoly.rootNear #p[-3, 0, 1] 1.7
-- All the roots at once, real ones first in increasing order:
#guard (ZPoly.algebraicRoots #p[-2, 0, 1]) == #[-s2, s2]

-- Arithmetic:
#guard (s2 + s3).p = #p[1, 0, -10, 0, 1]   -- the minimal polynomial of √2 + √3
-- Equality (without importing the Mathlib theory library,
-- you need to use `==`, but with it `=` is allowed too):
#guard (s2 + s3)⁻¹ == s3 - s2

/-- info: ZPoly.rootNear #p[1, 0, -10, 0, 1] 3.146264369 -/
#guard_msgs in
#eval s2 + s3

The arithmetic is exact, and the minimal polynomial is recomputed at each step. Equality is decidable: without the Mathlib theory library you compare with ==, and with it = is available too, because the companion proves the test correct.

A fixed number field

If you are working in one field rather than with individual numbers, QAdjoin is the field ℚ(a) generated by a canonical number, with elements stored as rational polynomials in it. Arithmetic is polynomial arithmetic modulo the minimal polynomial, with no root isolation at all, and inverses come from an extended gcd:

-- If you're working in a fixed number field, use `QAdjoin`: the field ℚ(a)
-- of a canonical number, whose elements are rational polynomials in it.
def cbrt2 : AlgebraicNumber := ZPoly.rootNear #p[-2, 0, 0, 1] 1.26
def c : QAdjoin cbrt2 := cbrt2.toQAdjoin

-- Arithmetic and equality are efficient in `QAdjoin`,
-- and inverses are calculated with extended GCDs.
#guard c ^ 3 == 2
#guard c⁻¹ == c * c / 2

-- Elements print as the expression that rebuilds them: the generating
-- number and the coordinates.
/-- info: QAdjoin.ofCoeffs (ZPoly.rootNear #p[-2, 0, 0, 1] 1.25992) #p[0, 0, 2] -/
#guard_msgs in
#eval c ^ 5

Elements print as the expression that rebuilds them, so a printed value pastes back and prints identically.

Towers

NumberTower builds ℚ(α₁, …, αₙ) one generator at a time, and factors over it with Trager's algorithm, which takes a norm to reduce the problem to factoring over the rationals:

-- `NumberTower.rat` is ℚ. `adjoin T a` extends the tower `T` by a root `a`;
-- the result carries the new tower, the adjoined generator `gen`, and the
-- inclusion `embed` of `T`, which is why its type names `T`.
def Q2 : Extension NumberTower.rat := adjoin NumberTower.rat s2.toRoot
def Q23 : Extension Q2.tower := adjoin Q2.tower s3.toRoot

def quartic (T : NumberTower) : Poly T := liftZPoly T #p[1, 0, -10, 0, 1]

-- Over ℚ(√2) the quartic splits into two quadratics; over ℚ(√2, √3) into
-- four linear factors. A factorization pairs each factor with its
-- multiplicity; here we read off the degrees.
#guard (factor Q2.tower (quartic Q2.tower)).factors.map
  (fun (g, _) => g.size - 1) = #[2, 2]
#guard (factor Q23.tower (quartic Q23.tower)).factors.map
  (fun (g, _) => g.size - 1) = #[1, 1, 1, 1]

The primitive element theorem is available as a function. flatten returns a single algebraic number generating the whole tower, together with the coordinate changes in each direction:

-- `flatten T : Flattening T` is the primitive element theorem as a function:
-- a single algebraic number generating the whole tower, with the coordinate
-- changes between the tower and ℚ(root). Here root is ±√2 ± √3, and
-- √2 = (root³ − 9·root)/2.
def F : Flattening Q23.tower := flatten Q23.tower

#guard F.root.p = #p[1, 0, -10, 0, 1]
#guard (F.toPrimitive (Q23.embed Q2.gen)).coeffs = #p[0, -9 / 2, 0, 1 / 2]

Arithmetic inside a tower is coordinate arithmetic over the basis, which is much cheaper than recomputing a minimal polynomial at every step:

-- Arithmetic in a tower is coordinate arithmetic: a power of √2 + √3 costs a
-- few multiplications of coordinate vectors, over the basis 1, √2, √3, √6.
def gamma : Elem Q23.tower := Q23.embed Q2.gen + Q23.gen

#guard coeffs (gamma ^ 10) = #[47525, 0, 0, 19402]   -- 47525 + 19402·√6

-- The same power as an `AlgebraicNumber` recomputes a minimal polynomial at
-- every step, and agrees. Its minimal polynomial is only quadratic, since the
-- power lies in ℚ(√6).
#guard (F.toPrimitive (gamma ^ 10)).toAlgebraicNumber == (s2 + s3) ^ 10

/-- info: ZPoly.rootNear #p[1, -95050, 1] 95049.99998947 -/
#guard_msgs in
#eval (s2 + s3) ^ 10

The Mathlib correspondence

HexNumberFieldMathlib proves these computations correct. It interprets each AlgebraicNumber as a complex number, and shows that interpretation is injective and preserves the arithmetic:

example (a b : AlgebraicNumber) (h : a.toComplex = b.toComplex) : a = b :=
  AlgebraicNumber.toComplex_injective h

example (a b : AlgebraicNumber) :
    (a + b).toComplex = a.toComplex + b.toComplex :=
  AlgebraicNumber.add_toComplex a b

The computational libraries are Mathlib-free; the *Mathlib libraries are the bridge, and hold the correspondence proofs. Everything is kernel-checkable, and nothing uses native_decide.

Discussion is welcome at #Computer algebra > Discussion: Hex on the Lean Zulip. The manual pages for HexNumberField and HexNumberFieldTower go into more detail, including the performance tables.