-
Notifications
You must be signed in to change notification settings - Fork 1
Pull requests: kim-em/hex-dev
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
docs(sparse-poly): Phase-7 manual chapter and READMEs
#9485
opened Aug 23, 2026 by
kim-em
Owner
Loading…
polish(sparse-poly): Phase-6 pass for the core and companion
#9483
opened Aug 23, 2026 by
kim-em
Owner
Loading…
feat(sparse-poly-mathlib): activate the companion with the complete Equiv surface
#9481
opened Aug 23, 2026 by
kim-em
Owner
Loading…
perf: build the disambiguation eliminant as a double resultant
#9432
opened Aug 22, 2026 by
kim-em
Owner
Loading…
bench: add the number-field pair's Phase-4 ladders, PARI comparator, and declarations
#9424
opened Aug 22, 2026 by
kim-em
Owner
Loading…
feat(sparse-poly): Phase-5 proof completion with the tree multiplication twin
#9413
opened Aug 22, 2026 by
kim-em
Owner
Loading…
feat(primality): add the HexPrimalityMathlib correspondence layer
#9412
opened Aug 22, 2026 by
kim-em
Owner
Loading…
feat(primality): wire the cube-root certificate arm
#9411
opened Aug 22, 2026 by
kim-em
Owner
Loading…
feat(primality): prove the cube-root Brillhart-Lehmer-Selfridge criterion
#9409
opened Aug 22, 2026 by
kim-em
Owner
Loading…
feat(primality): add the primality term elaborator and tactic
#9407
opened Aug 22, 2026 by
kim-em
Owner
Loading…
feat(sparse-poly): Phase-4 benchmarking, multiplication selection, and the headline report
#9406
opened Aug 22, 2026 by
kim-em
Owner
Loading…
feat(primality): add certificate search and the bounded decision API
#9402
opened Aug 22, 2026 by
kim-em
Owner
Loading…
feat(primality): add Brent rho and the internal partial factorization
#9401
opened Aug 22, 2026 by
kim-em
Owner
Loading…
feat(primality): add the Pocklington certificate and kernel-replayable checker
#9400
opened Aug 22, 2026 by
kim-em
Owner
Loading…
feat(sparse-poly): Phase-2 review fixes and the Phase-3 conformance suite
#9399
opened Aug 22, 2026 by
kim-em
Owner
Loading…
feat(primality): add Miller-Rabin with the proved compositeness direction
#9397
opened Aug 22, 2026 by
kim-em
Owner
Loading…
feat(primality): add the multiplicative order development
#9394
opened Aug 22, 2026 by
kim-em
Owner
Loading…
feat(bz): migrate hotPathCandidates onto the committed prime table
#9392
opened Aug 22, 2026 by
kim-em
Owner
Loading…
Previous Next
ProTip!
Mix and match filters to narrow down what you’re looking for.