Issues

• Add optional bounded native ECPP fallback to ordinary primality?

  kim-em/hex-dev#10674 · Filter by author kim-em opened on Oct 4, 2026
  1

• perf(rcf): normalize polynomials and quote reduced field elements in certificates

  kim-em/hex-dev#10634 · Filter by author kim-em opened on Oct 3, 2026
  1

• perf(sign-det): stop constructing a real algebraic number for every field-element sign

  kim-em/hex-dev#10635 · Filter by author kim-em opened on Oct 3, 2026
  2

  

• perf(rcf): decide field-element signs by interval evaluation, not one Sturm certificate each

  kim-em/hex-dev#10633 · Filter by author kim-em opened on Oct 3, 2026
  1

• Complete Sturm and real-algebraic prerequisite readiness for the real-closure family

  kim-em/hex-dev#10577 · Filter by author kim-em opened on Oct 2, 2026
  12

  

• Integrate and document the verified real-closure family; prepare split-package publication

  kim-em/hex-dev#10575 · Filter by author kim-em opened on Oct 2, 2026
  12

  

• Implement real-closure towers, transport and exploration with proofs

  kim-em/hex-dev#10378 · Filter by author kim-em opened on Sep 21, 2026
  68

  

• Implement BKR/Thom sign determination and checked replay

  kim-em/hex-dev#10377 · Filter by author kim-em opened on Sep 21, 2026
  172

  

• Implement rcf with real algebraic and certified constant coefficients

  kim-em/hex-dev#10358 · Filter by author kim-em opened on Sep 20, 2026
  75

  

• Implement the real-closure family through verified APIs and performance evidence

  kim-em/hex-dev#10331 · Filter by author kim-em opened on Sep 20, 2026
  44

• Implement hex-virtual-subst and its checked quantifier-elimination tactic

  kim-em/hex-dev#10329 · Filter by author kim-em opened on Sep 20, 2026

• perf(kronecker): cut the per-node kernel cost of the kronecker tactic on small identities

  kim-em/hex-dev#10287 · Filter by author kim-em opened on Sep 17, 2026
  

• feat(hex-gfq-mathlib): certify Conway minimality via compatible exponent classes

  kim-em/hex-dev#10119 · Filter by author kim-em opened on Sep 8, 2026

• feat(hex-conway): certify lexicographic minimality for low-degree entries

  kim-em/hex-dev#10118 · Filter by author kim-em opened on Sep 8, 2026

• feat(mv-factor): complete verified multivariate integer factorization and its Mathlib API

  enhancement
  kim-em/hex-dev#10082 · Filter by author kim-em opened on Sep 7, 2026
  9

  

• chore(nauty-ffi): expose automorphism generators, orbits and group order

  agent-planfeature
  kim-em/hex-dev#10025 · Filter by author kim-em opened on Sep 5, 2026

• feat(graph-iso): a tactic for automorphism and group-order goals

  agent-planblockedfeature
  kim-em/hex-dev#10024 · Filter by author kim-em opened on Sep 5, 2026

• perf(number-field-tower): give the dense toPrimitive map an admissible mode

  critical-pathfeature
  kim-em/hex-dev#9999 · Filter by author kim-em opened on Sep 5, 2026
  1

• perf(graph-iso): profile the large-n dense fast tier beyond refinement

  kim-em/hex-dev#9965 · Filter by author kim-em opened on Sep 3, 2026

• perf(number-field-tower): establish division evidence after inversion

  blockedcritical-pathfeature
  kim-em/hex-dev#9947 · Filter by author kim-em opened on Sep 3, 2026
  1

• perf(poly-fp): complete the Phase-4 evidence and FLINT comparator contract

  feature
  kim-em/hex-dev#9809 · Filter by author kim-em opened on Aug 28, 2026
  2

• directive(number-field-tower): integrate Phase-4 evidence and attest core

  blockedcritical-pathdirectivefeature
  kim-em/hex-dev#9665 · Filter by author kim-em opened on Aug 26, 2026
  8

• pod: planner lock sentinel

  coordination
  kim-em/hex-dev#1 · Filter by author kim-em opened on Apr 22, 2026
  26