hex

 Hex🔗

The hex project

hex is executable computer algebra for Lean 4: finite and number fields, polynomial factorization, root isolation, and lattice reduction. The computational core is Mathlib-free; Mathlib companions state correspondence contracts and, for mature libraries, supply their proofs.

Contents

  1. 1. HexBasic: shared dependency-free utilities
  2. 2. HexArith: low-level arithmetic foundations
  3. 3. HexPrimality: certified primality at scale
  4. 4. HexPoly: normalized dense polynomials
  5. 5. HexMvPoly: executable sparse multivariate polynomials
  6. 6. HexSparsePoly: sparse univariate polynomials
  7. 7. HexModArith: machine-word modular arithmetic
  8. 8. HexPolyFp: prime-field dense polynomials
  9. 9. HexPolyZ: integer dense polynomials
  10. 10. HexGFqRing: executable Fₚ quotient ring
  11. 11. HexHensel: executable Hensel lifting
  12. 12. HexRoots: certified complex-root isolation
  13. 13. HexRealRoots: certified real-root isolation
  14. 14. HexRCF: a decision procedure for univariate real arithmetic
  15. 15. HexMatrix: dense matrices and arithmetic
  16. 16. HexRowReduce: Gauss-Jordan reduction, span, and nullspace
  17. 17. HexBerlekamp: factorization over finite fields
  18. 18. HexGF2: packed GF(2) polynomials and GF(2ⁿ) fields
  19. 19. HexGFqField: executable GF(pⁿ)
  20. 20. HexConway: verified Conway-polynomial lookup
  21. 21. HexGFq: canonical finite-field constructors
  22. 22. HexDeterminant: the Leibniz determinant and cofactor theory
  23. 23. HexBareiss: the fraction-free determinant
  24. 24. HexResultant: subresultants and discriminants
  25. 25. HexGramSchmidt: Gram-Schmidt orthogonalization
  26. 26. HexLLL: lattice basis reduction
  27. 27. HexBerlekampZassenhaus: factorization over the integers
  28. 28. factor_poly and irreducibility: certified factoring
  29. 29. HexNumberField: exact algebraic numbers
  30. 30. HexNumberFieldTower: successive algebraic extensions
  31. 31. HexPermGroup: checked finite permutation groups
  32. 32. HexGraphIso: coloured graph canonical labelling
  33. 33. The nauty canonical labelling algorithm
  34. 34. Tutorials
  35. 35. Draft sections for unreleased libraries