ci: check Lean snippets in released READMEs

.github/workflows/ci.yml

@@ -168,7 +168,7 @@ jobs:
       # fresh against the restored libs, which is cheap.
       - name: Define the hex-dev cache + build target sets
         run: |
-          echo "HEX_LIB_TARGETS=HexBasic HexTruncatedSeries HexTruncatedSeriesMathlib HexArith HexPoly HexPolyFast HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexPrimality HexIntFactor HexPrimalityKernelProbe HexPrimalityElabProbe HexIntFactorKernelProbe HexMvGcdKernelProbe HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexHermite HexSmith HexCharPoly HexMinPoly HexPolySmith HexGramSchmidt HexLLL HexMatrixMathlib HexHermiteMathlib HexSmithMathlib HexSmithTests HexCharPolyMathlib HexMinPolyMathlib HexPolySmithMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexBerlekampZassenhausMathlibProofProbe HexBerlekampMathlibProofProbe HexPrimalityMathlib HexIntFactorMathlib HexPolyFpMathlib HexFactorizationModules HexRealRootsMathlib HexGF2Mathlib HexGFqMathlib HexMvPolyMathlib HexMvPolyMathlibProofProbe HexRCF HexRCFTests HexRootsMathlib HexResultantMathlib HexNumberField HexNumberFieldMathlib HexNumberFieldTower HexNumberFieldTowerMathlib HexReleaseTests HexReleaseExamples HexAggregateCheck" >> "$GITHUB_ENV"
+          echo "HEX_LIB_TARGETS=Hex HexBasic HexTruncatedSeries HexTruncatedSeriesMathlib HexArith HexPoly HexPolyFast HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexPrimality HexIntFactor HexPrimalityKernelProbe HexPrimalityElabProbe HexIntFactorKernelProbe HexMvGcdKernelProbe HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexHermite HexSmith HexCharPoly HexMinPoly HexPolySmith HexGramSchmidt HexLLL HexMatrixMathlib HexHermiteMathlib HexSmithMathlib HexSmithTests HexCharPolyMathlib HexMinPolyMathlib HexPolySmithMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexBerlekampZassenhausMathlibProofProbe HexBerlekampMathlibProofProbe HexPrimalityMathlib HexIntFactorMathlib HexPolyFpMathlib HexFactorizationModules HexRealRootsMathlib HexGF2Mathlib HexGFqMathlib HexMvPolyMathlib HexMvPolyMathlibProofProbe HexRCF HexRCFTests HexRootsMathlib HexResultantMathlib HexNumberField HexNumberFieldMathlib HexNumberFieldTower HexNumberFieldTowerMathlib HexReleaseTests HexReleaseExamples HexAggregateCheck" >> "$GITHUB_ENV"
           echo "HEX_EXE_TARGETS=hextruncatedseries_bench hexarith_bench hexpoly_bench hexpolyfast_bench hexpolysmith_bench hexmvpoly_bench hexmvgcd_bench hexsparsepoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexmodular_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexprimality_bench hexprimality_policy_probe hexprimality_fuel_probe hexintfactor_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexstrassen_compare hexdeterminant_bench hexbareiss_bench hexcharpoly_bench hexminpoly_bench hexgramschmidt_bench hexhermite_bench hexsmith_bench hexrealroots_bench hexrcf_bench hexroots_bench hexresultant_bench hexnumberfield_bench hexnumberfieldtower_bench hexinterval_decision_bench hexroots_demo hex_interval_representation_spike hex_interval_center_spike hex_interval_scale_spike hex_interval_scheduler_spike hex_interval_policy_frontier_spike hex_arith_floor hexlll_bench hexlll_gram_bench hexlll_external_reduction hexbz_factor_service" >> "$GITHUB_ENV"
       # Shared build. The libraries, bench exes, conformance #guard drivers, and
       # emit-fixture exes are all elaborated here so the two verification tails
@@ -212,6 +212,20 @@ jobs:
             hexnumberfieldtower_emit_fixtures
       - name: Build HexManual
         run: lake build HexManual
+      - name: Check README Lean snippets
+        run: |
+          for readme in Hex*/README.md; do
+            case "$readme" in
+              HexBareiss/README.md|HexBerlekampZassenhaus/README.md|HexBerlekampZassenhausMathlib/README.md)
+                lake exe lean-readme --prefix .lean-readme/Native.lean "$readme"
+                ;;
+              *)
+                lake exe lean-readme "$readme"
+                ;;
+            esac
+          done
+          lake exe lean-readme --prefix .lean-readme/Aggregate.lean \
+            scripts/release/hex-README.md
       # --- Parallel verification tails (single job, in-job parallel steps) ---
       # Both tails only read the already-built .lake/build; they write to
       # disjoint outputs, so they are safe to run concurrently. Each touches a

.lean-readme/Aggregate.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+import Lean
+public meta import HexLLL
+
+private def loadReadmeDynlib (dir stem : String) : IO Unit := do
+  let ext := if System.Platform.isOSX then "dylib" else "so"
+  Lean.loadDynlib s!".lake/build/lib/{dir}{stem}.{ext}"
+
+run_cmd loadReadmeDynlib "" "libhexarithffi"
+run_cmd loadReadmeDynlib "" "libHex_HexArith"
+run_cmd loadReadmeDynlib "" "libhexmodarithffi"
+run_cmd loadReadmeDynlib "" "libHex_HexModArith"
+run_cmd loadReadmeDynlib "lean/" "Hex_HexHensel_WordMul"
+run_cmd loadReadmeDynlib "" "libHex_HexBasic"
+run_cmd loadReadmeDynlib "" "libHex_HexMatrix"
+run_cmd loadReadmeDynlib "" "libHex_HexBareiss"

.lean-readme/Native.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+import Lean
+public meta import HexBareiss
+
+public section
+
+private def loadReadmeDynlib (dir stem : String) : IO Unit := do
+  let ext := if System.Platform.isOSX then "dylib" else "so"
+  Lean.loadDynlib s!".lake/build/lib/{dir}{stem}.{ext}"
+
+run_cmd loadReadmeDynlib "" "libhexarithffi"
+run_cmd loadReadmeDynlib "" "libHex_HexArith"
+run_cmd loadReadmeDynlib "" "libhexmodarithffi"
+run_cmd loadReadmeDynlib "" "libHex_HexModArith"
+run_cmd loadReadmeDynlib "lean/" "Hex_HexHensel_WordMul"
+run_cmd loadReadmeDynlib "" "libHex_HexBasic"
+run_cmd loadReadmeDynlib "" "libHex_HexMatrix"
+run_cmd loadReadmeDynlib "" "libHex_HexBareiss"

HexBareiss/README.md

@@ -74,15 +74,15 @@ Mathlib bridge proves quotient exactness implies agreement with the determinant.
 
 The public determinant agrees with the encoded data, `bareiss_eq_bareissData_det`:
 
-```lean
+```lean recall Hex.Matrix.bareiss_eq_bareissData_det
 theorem bareiss_eq_bareissData_det (M : Matrix Int n n) :
     bareiss M = (bareissData M).det
 ```
 
 The no-pivot run, when it reaches the final pivot without a singular step,
 reads off the last diagonal entry, `bareiss_eq_noPivotLoop_last_of_no_singular`:
 
-```lean
+```lean recall Hex.Matrix.bareiss_eq_noPivotLoop_last_of_no_singular
 theorem bareiss_eq_noPivotLoop_last_of_no_singular {k : Nat}
     (M : Matrix Int (k + 1) (k + 1))
     (h_no_sing :

HexBareissMathlib/README.md

@@ -72,22 +72,22 @@ the preferred compatibility surface and hold outright.
 The executable Bareiss determinant equals the Leibniz determinant,
 `bareiss_eq_det`:
 
-```lean
+```lean recall HexMatrixMathlib.bareiss_eq_det
 theorem bareiss_eq_det (M : Hex.Matrix Int n n) :
     Hex.Matrix.bareiss M = Hex.Matrix.det M
 ```
 
 It also equals Mathlib's determinant, `bareissDet_eq_det`:
 
-```lean
+```lean recall HexMatrixMathlib.bareissDet_eq_det
 theorem bareissDet_eq_det (M : Hex.Matrix Int n n) :
     Hex.Matrix.bareiss M = Matrix.det (matrixEquiv M)
 ```
 
 The Mathlib statement is proven directly by running the Bareiss loop and
 tracking the bordered-minor invariant step by step, `bareiss_eq_mathlib_det`:
 
-```lean
+```lean recall HexMatrixMathlib.bareiss_eq_mathlib_det
 theorem bareiss_eq_mathlib_det (M : Hex.Matrix Int n n) :
     Hex.Matrix.bareiss M = Matrix.det (matrixEquiv M)
 ```

HexConway/README.md

@@ -77,7 +77,7 @@ that the kernel replays; `native_decide` is not used anywhere. The aggregate
 dispatch theorem is `luebeckConwayPolynomial?_irreducible`, and the API-facing
 form is
 
-```lean
+```lean recall Hex.Conway.conwayPoly_irreducible
 theorem conwayPoly_irreducible
     (p n : Nat) [ZMod64.Bounds p] (h : SupportedEntry p n) :
     FpPoly.Irreducible (conwayPoly p n h)
@@ -89,7 +89,7 @@ as a negative control so the check is visibly not vacuous. The `Bool` is
 promoted to a statement about field elements, which is the well-definedness
 input a subfield embedding needs:
 
-```lean
+```lean recall Hex.Conway.eval_conwayPoly_subfieldGen_eq_zero
 theorem eval_conwayPoly_subfieldGen_eq_zero
     {p m n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p]
     (hm : SupportedEntry p m) (hn : SupportedEntry p n)

HexDeterminant/README.md

@@ -59,16 +59,19 @@ The headline theorem for each of the remaining results (with
 
 Column linearity, `det_setCol_add`:
 
-```lean
-theorem det_setCol_add (M : Matrix R n n) (dst : Fin n) (v w : Fin n → R) :
+```lean recall Hex.Matrix.det_setCol_add
+theorem det_setCol_add {R : Type u} [Lean.Grind.CommRing R] {n : Nat}
+    (M : Matrix R n n) (dst : Fin n) (v w : Fin n → R) :
     det (setCol M dst (fun r => v r + w r)) =
       det (setCol M dst v) + det (setCol M dst w)
 ```
 
 Laplace cofactor expansion along a row, `det_eq_finFoldl_laplace_row`:
 
-```lean
-theorem det_eq_finFoldl_laplace_row (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) :
+```lean recall Hex.Matrix.det_eq_finFoldl_laplace_row
+theorem det_eq_finFoldl_laplace_row
+    {R : Type u} [Lean.Grind.CommRing R] {n : Nat}
+    (M : Matrix R (n + 1) (n + 1)) (row : Fin (n + 1)) :
     det M =
       Fin.foldl (n + 1)
         (fun acc col => acc + M[row][col] * cofactor M row col) 0
@@ -86,8 +89,9 @@ their names apart. `det_setRow_setRow_mul_det` is the two-row replacement
 identity, the `2 × 2` case of Jacobi's adjugate-minor identity: for distinct
 rows `a`, `b` and arbitrary vectors `u`, `v`,
 
-```lean
+```lean recall Hex.Matrix.det_setRow_setRow_mul_det
 theorem det_setRow_setRow_mul_det
+    {R : Type u} [Lean.Grind.CommRing R] {n : Nat}
     (M : Matrix R (n + 1) (n + 1)) (a b : Fin (n + 1)) (hab : a ≠ b)
     (u v : Vector R (n + 1)) :
     det M * det (setRow (setRow M a u) b v) =

HexDeterminantMathlib/README.md

@@ -70,7 +70,7 @@ Desnanot-Jacobi.
 The determinant correspondence is fully proven over a `CommRing`. The
 headline theorem identifies the two determinants:
 
-```lean
+```lean recall HexMatrixMathlib.det_eq
 theorem det_eq [CommRing R] (M : Hex.Matrix R n n) :
     Hex.Matrix.det M = Matrix.det (matrixEquiv M)
 ```
@@ -79,7 +79,7 @@ The unrestricted three-term Grassmann-Plücker relation, for any three ordered
 rows `p1 < p2 < p3` (`hex-determinant` proves the Mathlib-free specialisation
 where `p2` and `p3` are the last two rows):
 
-```lean
+```lean recall HexMatrixMathlib.det_plucker_three_term
 theorem det_plucker_three_term
     {R : Type u} [CommRing R] {n : Nat}
     (B : Hex.Matrix R (n + 3) (n + 1)) (v : Vector R (n + 3))
@@ -92,7 +92,7 @@ theorem det_plucker_three_term
 
 The Desnanot-Jacobi identity over Mathlib matrices:
 
-```lean
+```lean recall desnanot_jacobi
 theorem desnanot_jacobi {R : Type*} [CommRing R] {n : ℕ}
     (M : Matrix (Fin (n + 2)) (Fin (n + 2)) R) :
     M.det * (M.submatrix (Fin.succAbove 0 ∘ (Fin.last n).succAbove)

HexGF2/README.md

@@ -69,10 +69,12 @@ Irreducibility is proved rather than tabulated. The Rabin test is sound, and so
 is certificate replay, which is what lets a committed modulus be checked by the
 kernel without `native_decide`:
 
-```lean
+```lean recall Hex.GF2Poly.rabinTest_imp_irreducible
 theorem rabinTest_imp_irreducible (f : GF2Poly) (hrabin : rabinTest f = true) :
     GF2Poly.Irreducible f
+```
 
+```lean recall Hex.GF2Poly.checkIrreducibilityCertificate_imp_irreducible
 theorem checkIrreducibilityCertificate_imp_irreducible
     (f : GF2Poly) (cert : IrreducibilityCertificate)
     (hcheck : checkIrreducibilityCertificate f cert = true) :
@@ -85,10 +87,9 @@ laws need more: `GF2Poly.Irreducible` is satisfied by the constant `1`, and the
 quotient by a constant is trivial, so nonconstancy is a separate hypothesis and
 the field laws are functions rather than instances.
 
-```lean
-def fieldOfDegreePos (hdeg : 0 < f.degree) : Lean.Grind.Field (GF2nPoly f hirr)
-
-theorem isCharPOfDegreePos (hdeg : 0 < f.degree) :
+```lean recall Hex.GF2nPoly.isCharPOfDegreePos
+theorem isCharPOfDegreePos {f : GF2Poly} {hirr : GF2Poly.Irreducible f}
+    (hdeg : 0 < f.degree) :
     Lean.Grind.IsCharP (GF2nPoly f hirr) 2
 ```
 

HexGF2Mathlib/README.md

@@ -75,6 +75,10 @@ The equivalences are the content. The packed polynomial representation
 corresponds to the generic one, and composing reaches Mathlib:
 
 ```lean
+import HexGF2Mathlib
+
+open Hex
+
 def equiv : Hex.GF2Poly ≃+* Hex.FpPoly 2
 
 noncomputable def equivPolynomial : Hex.GF2Poly ≃+* Polynomial (ZMod 2)
@@ -92,20 +96,16 @@ recursive Bezout theorem with the executable packed gcd.
 
 The single-word wrapper, in namespace `HexGF2Mathlib.GF2n`:
 
-```lean
-def equiv : Hex.GF2n n irr hn hn64 hirr ≃+*
-    GenericFiniteField (n := n) (irr := irr) (hn := hn) (hn64 := hn64) (hirr := hirr)
-
-theorem fintype_card :
+```lean recall HexGF2Mathlib.GF2n.fintype_card
+theorem fintype_card {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64}
+    {hirr : Hex.GF2Poly.Irreducible (Hex.GF2Poly.ofUInt64Monic irr n)} :
     Fintype.card (Hex.GF2n n irr hn hn64 hirr) = 2 ^ n
 ```
 
 The arbitrary-degree wrapper, in namespace `HexGF2Mathlib.GF2nPoly`:
 
-```lean
-def equiv : Hex.GF2nPoly f hirr ≃+* GenericFiniteField (f := f) (hirr := hirr) (hdeg := hdeg)
-
-theorem fintype_card :
+```lean recall HexGF2Mathlib.GF2nPoly.fintype_card
+theorem fintype_card {f : Hex.GF2Poly} {hirr : Hex.GF2Poly.Irreducible f} :
     Fintype.card (Hex.GF2nPoly f hirr) = 2 ^ f.degree
 ```
 

HexGFq/README.md

@@ -73,6 +73,10 @@ The field type is built directly from the Conway table's proofs, so a `GFq`
 that elaborates is a field:
 
 ```lean
+import HexGFq
+
+open Hex
+
 abbrev GFq (p n : Nat) [ZMod64.Bounds p] (h : Conway.SupportedEntry p n) : Type :=
   GFqField.FiniteField (Conway.conwayPoly p n h)
     (Conway.conwayPoly_nonconstant p n h)
@@ -92,6 +96,10 @@ modulus, replayed from a Rabin certificate by the kernel, and a proof that the
 packed word denotes the same polynomial as the committed Conway entry:
 
 ```lean
+import HexGFq
+
+open Hex Hex.GFq Hex.Conway
+
 class PackedGF2Entry (n : Nat) where
   entry : SupportedEntry 2 n
   lower : UInt64

HexGFqField/README.md

@@ -71,8 +71,9 @@ example : frob α = α ^ 5 := frob_eq_pow α
 The field laws are proved, not asserted. Inverse cancellation is the result the
 rest rests on:
 
-```lean
+```lean recall Hex.GFqField.mul_inv_cancel
 theorem mul_inv_cancel
+    {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Hex.Nat.Prime p}
     {f : FpPoly p} {hf : 0 < FpPoly.degree f} {hirr : FpPoly.Irreducible f}
     {x : FiniteField f hf hp hirr} (hx : x ≠ 0) :
     x * x⁻¹ = 1
@@ -85,6 +86,10 @@ already carries both the irreducibility proof and the positive-degree
 hypothesis:
 
 ```lean
+import HexGFqField
+
+open Hex Hex.GFqField
+
 instance {f : FpPoly p} {hf : 0 < FpPoly.degree f} {hirr : FpPoly.Irreducible f} :
     Lean.Grind.Field (FiniteField f hf hp hirr)
 

HexGFqMathlib/README.md

@@ -70,11 +70,9 @@ example {p n : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p]
 The executable field carries Mathlib's `Field` structure, and the carrier is
 finite with the cardinality its construction promises:
 
-```lean
-noncomputable instance field :
-    Field (Hex.GFqField.FiniteField f hf hp hirr)
-
-theorem fintype_card_eq_pow (h : Hex.Conway.SupportedEntry p n) :
+```lean recall HexGFqMathlib.GFq.fintype_card_eq_pow
+theorem fintype_card_eq_pow {p n : Nat} [Hex.ZMod64.Bounds p]
+    (h : Hex.Conway.SupportedEntry p n) :
     Fintype.card (Hex.GFq p n h) = p ^ n
 ```
 
@@ -88,7 +86,12 @@ that the two counts agree, so it needs `Fact p.Prime` and `n ≠ 0` as
 hypotheses, neither of which the executable side carries:
 
 ```lean
-noncomputable def equivGaloisField [Fact p.Prime]
+import HexGFqMathlib
+
+open Hex
+
+noncomputable def equivGaloisField {p n : Nat} [Hex.ZMod64.Bounds p]
+    [Hex.ZMod64.PrimeModulus p] [Fact p.Prime]
     (h : Hex.Conway.SupportedEntry p n) (hn : n ≠ 0) :
     _root_.RingEquiv (Hex.GFq p n h) (GaloisField p n)
 ```
@@ -98,6 +101,10 @@ built on hex-gf2-mathlib's `GF2n.equiv` and computable, the second inheriting
 the choice `ringEquivOfCardEq` makes:
 
 ```lean
+import HexGFqMathlib
+
+open Hex
+
 def equivGFq : RingEquiv (GF2q n) (GFq 2 n h.entry)
 
 noncomputable def equivGaloisField : RingEquiv (GF2q n) (GaloisField 2 n)
@@ -107,6 +114,10 @@ The subfield embedding is a genuine ring homomorphism, on a committed divisor
 pair carrying a `Conway.Compatible` witness rather than a bare `m ∣ n` proof:
 
 ```lean
+import HexGFqMathlib
+
+open Hex
+
 noncomputable def conwayEmbed (p m n : Nat) [Hex.ZMod64.Bounds p]
     [Hex.ZMod64.PrimeModulus p]
     (hm : Hex.Conway.SupportedEntry p m) (hn : Hex.Conway.SupportedEntry p n)

HexGramSchmidt/README.md

@@ -71,7 +71,7 @@ lower-unitriangular coefficient matrix) are available over both rings.
 The orthogonalization theory is proven over the Mathlib-free integer and
 rational cores. The orthogonal basis, `basis_orthogonal`:
 
-```lean
+```lean recall Hex.GramSchmidt.Int.basis_orthogonal
 theorem basis_orthogonal (b : Matrix Int n m)
     (i j : Nat) (hi : i < n) (hj : j < n) (hij : i ≠ j) :
     ((basis b).row ⟨i, hi⟩).dotProduct ((basis b).row ⟨j, hj⟩) = 0
@@ -82,7 +82,7 @@ coefficient laws `coeffs_diag` and `coeffs_upper`, the span equality
 `basis_span`, and the update laws for `sizeReduce` and `adjacentSwap`. The
 key lattice estimate, `normSq_latticeVec_ge_min_basis_normSq`:
 
-```lean
+```lean recall Hex.GramSchmidt.Int.normSq_latticeVec_ge_min_basis_normSq
 theorem normSq_latticeVec_ge_min_basis_normSq
     (b : Matrix Int n m) (_hli : independent b)
     (v : Vector Int m) (hv : memLattice b v) (hv' : v ≠ 0) :