ci: free up runner disk space before build

.github/workflows/ci.yml

@@ -2,12 +2,24 @@ name: CI
 
 on:
   push:
+    branches: [main]
   pull_request:
 
 jobs:
   verify:
     runs-on: ubuntu-latest
     steps:
+      - name: Free up disk space
+        uses: jlumbroso/free-disk-space@v1.3.1
+        with:
+          tool-cache: false
+          android: true
+          dotnet: true
+          haskell: true
+          large-packages: true
+          docker-images: true
+          swap-storage: true
+
       - uses: actions/checkout@v4
         with:
           fetch-depth: 0
@@ -126,5 +138,45 @@ jobs:
       - name: Verify Generated Output
         run: python scripts/generate_projects.py --check
 
+      # Detect whether generated/ files changed to skip the expensive
+      # workspace build step on PRs that only touch problem sources or
+      # manifests.
+      - name: Detect generated workspace changes
+        id: changes
+        run: |
+          BASE="${{ github.event.pull_request.base.sha || github.event.before }}"
+          if [ "$BASE" = "0000000000000000000000000000000000000000" ]; then
+            echo "generated_changed=true" >> "$GITHUB_OUTPUT"
+          elif git diff --name-only "$BASE"..HEAD | grep -q '^generated/'; then
+            echo "generated_changed=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "generated_changed=false" >> "$GITHUB_OUTPUT"
+          fi
+
+      # Download Mathlib cache once in the first workspace, then hard-link
+      # its .lake/packages tree into every other workspace so that each
+      # subsequent `lake build` skips the ~2 GB download + decompression.
+      - name: Prepare shared Mathlib cache for workspaces
+        if: steps.changes.outputs.generated_changed == 'true'
+        run: |
+          set -euo pipefail
+          FIRST=$(find generated -maxdepth 1 -mindepth 1 -type d -exec test -f '{}/lakefile.toml' \; -print | sort | head -1)
+          if [ -z "$FIRST" ]; then
+            echo "No generated workspaces found; skipping."
+            exit 0
+          fi
+          echo "==> Fetching Mathlib cache in $FIRST"
+          (cd "$FIRST" && lake update && lake exe cache get)
+          for ws in generated/*/; do
+            [ -f "${ws}lakefile.toml" ] || continue
+            [ "$(realpath "$ws")" = "$(realpath "$FIRST/")" ] && continue
+            echo "==> Linking Mathlib packages into $ws"
+            mkdir -p "${ws}.lake"
+            rm -rf "${ws}.lake/packages"
+            cp -al "${FIRST}/.lake/packages" "${ws}.lake/packages"
+            cp "${FIRST}/lake-manifest.json" "${ws}lake-manifest.json"
+          done
+
       - name: Build Generated Workspaces
+        if: steps.changes.outputs.generated_changed == 'true'
         run: python scripts/check_generated_builds.py

generated/chudnovsky_formula_for_pi_inv/lakefile.toml

@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"

generated/cyclotomic_integer_house_between_two_and_76_33/lakefile.toml

@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"

generated/cyclotomic_integer_house_le_two/lakefile.toml

@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"

generated/dvd_card_connectedComponent_markoffGraph/Challenge.lean

@@ -1,5 +1,6 @@
 import ChallengeDeps
 
+open LeanEval.Combinatorics
 open scoped BigOperators
 
 theorem dvd_card_connectedComponent_markoffGraph {p : ℕ} (hp : Nat.Prime p) (hgt : 3 < p) :

generated/dvd_card_connectedComponent_markoffGraph/Solution.lean

@@ -1,6 +1,7 @@
 import ChallengeDeps
 import Submission
 
+open LeanEval.Combinatorics
 open scoped BigOperators
 
 theorem dvd_card_connectedComponent_markoffGraph {p : ℕ} (hp : Nat.Prime p) (hgt : 3 < p) :

generated/dvd_card_connectedComponent_markoffGraph/Submission.lean

@@ -1,6 +1,7 @@
 import ChallengeDeps
 import Submission.Helpers
 
+open LeanEval.Combinatorics
 open scoped BigOperators
 
 namespace Submission

generated/dvd_card_connectedComponent_markoffGraph/lakefile.toml

@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "ChallengeDeps"

generated/e8_irrep_tensor_square_decomp/Challenge.lean

@@ -0,0 +1,13 @@
+import ChallengeDeps
+
+open LeanEval.RepresentationTheory
+open scoped TensorProduct
+
+theorem e8_irrep_tensor_square_decomp :
+    ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V)
+      (_ : LieRingModule (LieAlgebra.e₈ ℂ) V) (_ : LieModule ℂ (LieAlgebra.e₈ ℂ) V),
+      Module.finrank ℂ V = 779247 ∧
+      LieModule.IsIrreducible ℂ (LieAlgebra.e₈ ℂ) V ∧
+      (isotypicComponents (UniversalEnvelopingAlgebra ℂ (LieAlgebra.e₈ ℂ))
+        (V ⊗[ℂ] V)).ncard = 40 := by
+  sorry

generated/e8_irrep_tensor_square_decomp/ChallengeDeps.lean

@@ -0,0 +1,37 @@
+import Mathlib
+
+namespace LeanEval
+namespace RepresentationTheory
+
+open scoped TensorProduct
+
+/-!
+Tensor square decomposition for irreducible representations of g₂ and e₈
+defined by the Serre construction.
+
+For each of the exceptional Lie algebras g₂ and e₈ over ℂ, the irreducible
+representation with highest weight `ω₁ + ω_n` (the sum of the first and last
+fundamental weights, in Bourbaki labelling) has a particular dimension `d`,
+and its tensor square decomposes into `k` isotypic components (counted as
+distinct isomorphism classes of irreducible Lie submodules):
+
+* g₂: dim V = 64,     k = 14   (highest weight ω₁ + ω₂)
+* e₈: dim V = 779247, k = 40   (highest weight ω₁ + ω₈)
+
+Mathlib's `isotypicComponents` is defined for modules over a ring. To use it
+on a Lie module `M`, we transport the action through the universal enveloping
+algebra: a `LieModule R L M` extends to a `Module (UniversalEnvelopingAlgebra R L) M`
+via the universal property.
+-/
+
+noncomputable instance lieModuleToEnvelopingModule
+    (R L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
+    [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
+    Module (UniversalEnvelopingAlgebra R L) M :=
+  Module.compHom M
+    (UniversalEnvelopingAlgebra.lift R (LieModule.toEnd R L M)).toRingHom
+
+
+
+end RepresentationTheory
+end LeanEval

generated/e8_irrep_tensor_square_decomp/README.md

@@ -0,0 +1,25 @@
+# `e8_irrep_tensor_square_decomp`
+
+Tensor square decomposition of a 779247-dim irreducible e₈-representation
+
+- Problem ID: `e8_irrep_tensor_square_decomp`
+- Test Problem: no
+- Submitter: Kim Morrison
+- Notes: e₈ is the largest exceptional Lie algebra (dim 248), defined here by the Serre construction (Mathlib's `LieAlgebra.e₈`). The relevant irreducible representation has highest weight ω₁ + ω₈ (the sum of the first and last fundamental weights, in Bourbaki labelling), dimension 779247; its tensor square decomposes into 40 isomorphism classes of irreducible Lie submodules. The U(g)-module structure on V ⊗ V used in the statement comes from lifting the Lie action via the universal enveloping algebra.
+- Source: Classical: representation theory of the exceptional Lie algebra e₈.
+- Informal solution: Construct V as V(ω₁+ω₈), the unique 779247-dim irrep of e₈. Tensor square (LiE-verified) has 40 distinct simple summand isomorphism classes (155 components with multiplicity), with the smallest being the trivial 1-dim, the 248-dim adjoint (mult 2), the 3875-dim V(ω₁), and so on up to the 85,424,220,000-dim summand.
+
+Do not modify `Challenge.lean` or `Solution.lean`. Those files are part of the
+trusted benchmark and fixed by the repository.
+
+Write your solution in `Submission.lean` and any additional local modules under
+`Submission/`.
+
+Participants may use Mathlib freely. Any helper code not already available in
+Mathlib must be inlined into the submission workspace.
+
+Multi-file submissions are allowed through `Submission.lean` and additional local
+modules under `Submission/`.
+
+`lake test` runs comparator for this problem. The command expects a comparator
+binary in `PATH`, or in the `COMPARATOR_BIN` environment variable.

generated/e8_irrep_tensor_square_decomp/Solution.lean

@@ -0,0 +1,14 @@
+import ChallengeDeps
+import Submission
+
+open LeanEval.RepresentationTheory
+open scoped TensorProduct
+
+theorem e8_irrep_tensor_square_decomp :
+    ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V)
+      (_ : LieRingModule (LieAlgebra.e₈ ℂ) V) (_ : LieModule ℂ (LieAlgebra.e₈ ℂ) V),
+      Module.finrank ℂ V = 779247 ∧
+      LieModule.IsIrreducible ℂ (LieAlgebra.e₈ ℂ) V ∧
+      (isotypicComponents (UniversalEnvelopingAlgebra ℂ (LieAlgebra.e₈ ℂ))
+        (V ⊗[ℂ] V)).ncard = 40 := by
+  exact Submission.e8_irrep_tensor_square_decomp

generated/e8_irrep_tensor_square_decomp/Submission.lean

@@ -0,0 +1,18 @@
+import ChallengeDeps
+import Submission.Helpers
+
+open LeanEval.RepresentationTheory
+open scoped TensorProduct
+
+namespace Submission
+
+theorem e8_irrep_tensor_square_decomp :
+    ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V)
+      (_ : LieRingModule (LieAlgebra.e₈ ℂ) V) (_ : LieModule ℂ (LieAlgebra.e₈ ℂ) V),
+      Module.finrank ℂ V = 779247 ∧
+      LieModule.IsIrreducible ℂ (LieAlgebra.e₈ ℂ) V ∧
+      (isotypicComponents (UniversalEnvelopingAlgebra ℂ (LieAlgebra.e₈ ℂ))
+        (V ⊗[ℂ] V)).ncard = 40 := by
+  sorry
+
+end Submission

generated/e8_irrep_tensor_square_decomp/Submission/Helpers.lean

@@ -0,0 +1,3 @@
+namespace Submission.Helpers
+
+end Submission.Helpers

generated/e8_irrep_tensor_square_decomp/WorkspaceTest.lean

@@ -0,0 +1,38 @@
+import Lean
+
+open Lean
+
+def comparatorExists (comparatorBin : String) : IO Bool := do
+  if comparatorBin.contains '/' then
+    return (← System.FilePath.pathExists comparatorBin)
+  try
+    let child ← IO.Process.spawn {
+      cmd := "sh"
+      args := #["-c", "command -v \"$1\" >/dev/null 2>&1", "sh", comparatorBin]
+    }
+    let exitCode ← child.wait
+    return exitCode == 0
+  catch _ =>
+    return false
+
+def main : IO UInt32 := do
+  let comparatorBin := (← IO.getEnv "COMPARATOR_BIN").getD "comparator"
+  if !(← comparatorExists comparatorBin) then
+    IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
+    IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
+    IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
+    pure 1
+  else
+    try
+      let child ← IO.Process.spawn {
+        cmd := "lake"
+        args := #["env", comparatorBin, "config.json"]
+      }
+      let exitCode ← child.wait
+      pure exitCode
+    catch err =>
+      IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
+      IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
+      IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
+      IO.eprintln s!"Original error: {err}"
+      pure 1

generated/e8_irrep_tensor_square_decomp/config.json

@@ -0,0 +1,13 @@
+{
+  "challenge_module": "Challenge",
+  "solution_module": "Solution",
+  "theorem_names": [
+    "e8_irrep_tensor_square_decomp"
+  ],
+  "permitted_axioms": [
+    "propext",
+    "Quot.sound",
+    "Classical.choice"
+  ],
+  "enable_nanoda": false
+}

generated/e8_irrep_tensor_square_decomp/lakefile.toml

@@ -0,0 +1,27 @@
+name = "e8_irrep_tensor_square_decomp"
+testDriver = "workspace_test"
+defaultTargets = ["Challenge", "Solution", "Submission"]
+
+[leanOptions]
+autoImplicit = false
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "50d5513e83c"
+
+[[lean_lib]]
+name = "ChallengeDeps"
+
+[[lean_lib]]
+name = "Challenge"
+
+[[lean_lib]]
+name = "Solution"
+
+[[lean_lib]]
+name = "Submission"
+
+[[lean_exe]]
+name = "workspace_test"
+root = "WorkspaceTest"

generated/e8_irrep_tensor_square_decomp/lean-toolchain

@@ -0,0 +1,2 @@
+leanprover/lean4:v4.30.0-rc1
+

generated/exists_complementary_polynomial_on_unit_circle/lakefile.toml

@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"

generated/finite_graph_ramsey_theorem/lakefile.toml

@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"

generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/lakefile.toml

@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"

generated/g2_irrep_tensor_square_decomp/Challenge.lean

@@ -0,0 +1,13 @@
+import ChallengeDeps
+
+open LeanEval.RepresentationTheory
+open scoped TensorProduct
+
+theorem g2_irrep_tensor_square_decomp :
+    ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V)
+      (_ : LieRingModule (LieAlgebra.g₂ ℂ) V) (_ : LieModule ℂ (LieAlgebra.g₂ ℂ) V),
+      Module.finrank ℂ V = 64 ∧
+      LieModule.IsIrreducible ℂ (LieAlgebra.g₂ ℂ) V ∧
+      (isotypicComponents (UniversalEnvelopingAlgebra ℂ (LieAlgebra.g₂ ℂ))
+        (V ⊗[ℂ] V)).ncard = 14 := by
+  sorry