⋆_G Tensor Algebra: Lean 4 Formalization
Lean 4 + Mathlib formalization of the proofs from:
Group-Algebraic Tensors: Optimal Equivariant Learning and Physical Symmetry Discovery Hoyos, Ubaru, Huh, Kalantzis, Clarkson, Kilmer, Avron, Horesh
Status
- 0 sorry across all 6 modules (600 lines total)
- 5 axioms, all standard textbook results not yet in Mathlib
Prerequisites
Install elan (the Lean version manager):
curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh
source ~/.profile
Building
Option A: Use the build script (recommended)
cd starG-lean
./build.sh
This automatically fetches Mathlib, syncs the Lean toolchain version, downloads prebuilt caches, and builds the project.
Option B: Manual steps
cd starG-lean
# 1. Fetch Mathlib
lake update
# 2. IMPORTANT: Sync toolchain to match Mathlib's requirement.
# Without this step you will get version mismatch errors.
cp .lake/packages/mathlib/lean-toolchain ./lean-toolchain
# 3. Download prebuilt Mathlib .olean files (avoids multi-hour rebuild)
lake exe cache get
# 4. Build
lake build
Troubleshooting
"unknown module prefix 'Mathlib'", You need to run lake update first.
Mathlib is not bundled; it is fetched from GitHub.
"no such file or directory ... Mathlib/...", Toolchain version mismatch.
Run: cp .lake/packages/mathlib/lean-toolchain ./lean-toolchain
then: lake exe cache get && lake build
"toolchain 'leanprover/lean4:vX.Y.Z' is not installed", elan will auto-install it. Just run the command again.
Starting fresh:
rm -rf .lake lake-packages
./build.sh
Architecture
| File | Lines | Paper Section |
|---|---|---|
Basic.lean |
109 | SI 1-4: convolution tensor, star product, transpose, identity |
Algebra.lean |
135 | SI 4: associativity, distributivity, identity, transpose |
ProductGroup.lean |
137 | Theorem 2: product group factorization, Kronecker irreps |
Equivariance.lean |
146 | SI 7: equivariance, Frobenius/Fourier power invariance |
WignerEckart.lean |
155 | 2.5: octahedral irreps, CG multiplicities, selection rules |
SVD.lean |
215 | Theorem 1: SVD existence, Eckart-Young optimality |
Axioms (5, all in SVD.lean)
| # | Axiom | Reference |
|---|---|---|
| 1 | matrix_best_rank_k_approx |
Eckart and Young 1936 |
| 2 | parseval_group |
Serre, Linear Reps of Finite Groups, 2.4 |
| 3 | fourier_multiplicative |
Terras, Fourier Analysis on Finite Groups, Ch. 7 |
| 4 | fourier_injective |
Peter-Weyl completeness |
| 5 | fourier_surjective |
Peter-Weyl + Fourier inversion |