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. HexArith: low-level arithmetic foundations
  2. 2. HexPoly: normalized dense polynomials
  3. 3. HexMvPoly: executable sparse multivariate polynomials
  4. 4. HexModArith: machine-word modular arithmetic
  5. 5. HexPolyFp: prime-field dense polynomials
  6. 6. HexPolyZ: integer dense polynomials
  7. 7. HexGFqRing: executable Fₚ quotient ring
  8. 8. HexHensel: executable Hensel lifting
  9. 9. HexRoots: certified complex-root isolation
  10. 10. HexRealRoots: certified real-root isolation
  11. 11. HexMatrix: dense matrices and arithmetic
  12. 12. HexRowReduce: Gauss-Jordan reduction, span, and nullspace
  13. 13. HexBerlekamp: factorization over finite fields
  14. 14. HexDeterminant: the Leibniz determinant and cofactor theory
  15. 15. HexBareiss: the fraction-free integer determinant
  16. 16. HexGramSchmidt: Gram-Schmidt orthogonalization
  17. 17. HexLLL: lattice basis reduction
  18. 18. HexBerlekampZassenhaus: factorization over the integers
  19. 19. factor_poly and irreducibility: certified factoring
  20. 20. Tutorials
  21. 21. Draft sections for unreleased libraries