coxeter-groups

A tour in the wonderland of math with python.

Visualize 3d/4d hyperbolic honeycombs and Boyd-Maxwell sphere packings.

Cluster algebraic/geometric structures related to plabic graphs

Coxeter groups in Lean 4

SageMath implementation of the restricted permutahedral model for computing the topology (cohomology, cup product, fundamental groups, asphericity criteria) of real parabolic arrangement complements associated to finite Coxeter groups.

ML Clifford invariants of Coxeter elements (arXiv: 2310.00041)

Pure-math E8/H4 polytope geometry + projection toolkit for TypeScript — root systems, Petrie/Moxness/H4 stereographic projections, platonic-hull extraction, fold-morph interpolation. Apache-2.0.

A tool to find virtual algebraic fibrations of right-angled Coxeter groups.

58 fundamental constants derived from E₈ → H₄ icosahedral geometry with zero free parameters — includes a self-sustaining solver and falsifiable predictions.

Twisted conjugacy in spherical Artin groups and their crystallographic quotients: every irreducible spherical Artin group of rank ≥ 2 has property R∞, but its crystallographic quotient need not (Reidemeister number 18 in type I₂(5)). Paper, Lean formalisation, and exact computational certificates.

Lean 4 proofs that the rank-two Coxeter group I₂(m+2) is the dihedral group of order 2(m+2), checked against Mathlib's own Coxeter and dihedral objects, with exact integral certificates for the finite and affine rank-two cases.

Offline-capable Coxeter Cayley/Davis/Y_Gamma research and teaching viewer