diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 752521dcb..dd15c6c2b 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/generated/chudnovsky_formula_for_pi_inv/lakefile.toml b/generated/chudnovsky_formula_for_pi_inv/lakefile.toml index 8d5b5b368..e940c4114 100644 --- a/generated/chudnovsky_formula_for_pi_inv/lakefile.toml +++ b/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" diff --git a/generated/cyclotomic_integer_house_between_two_and_76_33/lakefile.toml b/generated/cyclotomic_integer_house_between_two_and_76_33/lakefile.toml index 1e024a527..428a4fd1f 100644 --- a/generated/cyclotomic_integer_house_between_two_and_76_33/lakefile.toml +++ b/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" diff --git a/generated/cyclotomic_integer_house_le_two/lakefile.toml b/generated/cyclotomic_integer_house_le_two/lakefile.toml index e3df9754b..9a60b9291 100644 --- a/generated/cyclotomic_integer_house_le_two/lakefile.toml +++ b/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" diff --git a/generated/dvd_card_connectedComponent_markoffGraph/Challenge.lean b/generated/dvd_card_connectedComponent_markoffGraph/Challenge.lean index 876808047..a7d92b5e9 100644 --- a/generated/dvd_card_connectedComponent_markoffGraph/Challenge.lean +++ b/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) : diff --git a/generated/dvd_card_connectedComponent_markoffGraph/Solution.lean b/generated/dvd_card_connectedComponent_markoffGraph/Solution.lean index 498c0f2af..bf53c696b 100644 --- a/generated/dvd_card_connectedComponent_markoffGraph/Solution.lean +++ b/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) : diff --git a/generated/dvd_card_connectedComponent_markoffGraph/Submission.lean b/generated/dvd_card_connectedComponent_markoffGraph/Submission.lean index bdfa7f508..ab314ffcb 100644 --- a/generated/dvd_card_connectedComponent_markoffGraph/Submission.lean +++ b/generated/dvd_card_connectedComponent_markoffGraph/Submission.lean @@ -1,6 +1,7 @@ import ChallengeDeps import Submission.Helpers +open LeanEval.Combinatorics open scoped BigOperators namespace Submission diff --git a/generated/dvd_card_connectedComponent_markoffGraph/lakefile.toml b/generated/dvd_card_connectedComponent_markoffGraph/lakefile.toml index 32b324cf9..bdf9e3455 100644 --- a/generated/dvd_card_connectedComponent_markoffGraph/lakefile.toml +++ b/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" diff --git a/generated/e8_irrep_tensor_square_decomp/Challenge.lean b/generated/e8_irrep_tensor_square_decomp/Challenge.lean new file mode 100644 index 000000000..02c7c2df3 --- /dev/null +++ b/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 diff --git a/generated/e8_irrep_tensor_square_decomp/ChallengeDeps.lean b/generated/e8_irrep_tensor_square_decomp/ChallengeDeps.lean new file mode 100644 index 000000000..9952fda9b --- /dev/null +++ b/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 diff --git a/generated/e8_irrep_tensor_square_decomp/README.md b/generated/e8_irrep_tensor_square_decomp/README.md new file mode 100644 index 000000000..64ef5330b --- /dev/null +++ b/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. diff --git a/generated/e8_irrep_tensor_square_decomp/Solution.lean b/generated/e8_irrep_tensor_square_decomp/Solution.lean new file mode 100644 index 000000000..7d9aacece --- /dev/null +++ b/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 diff --git a/generated/e8_irrep_tensor_square_decomp/Submission.lean b/generated/e8_irrep_tensor_square_decomp/Submission.lean new file mode 100644 index 000000000..7b8853ab0 --- /dev/null +++ b/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 diff --git a/generated/e8_irrep_tensor_square_decomp/Submission/Helpers.lean b/generated/e8_irrep_tensor_square_decomp/Submission/Helpers.lean new file mode 100644 index 000000000..1561e7c8a --- /dev/null +++ b/generated/e8_irrep_tensor_square_decomp/Submission/Helpers.lean @@ -0,0 +1,3 @@ +namespace Submission.Helpers + +end Submission.Helpers diff --git a/generated/e8_irrep_tensor_square_decomp/WorkspaceTest.lean b/generated/e8_irrep_tensor_square_decomp/WorkspaceTest.lean new file mode 100644 index 000000000..ecb65777d --- /dev/null +++ b/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 diff --git a/generated/e8_irrep_tensor_square_decomp/config.json b/generated/e8_irrep_tensor_square_decomp/config.json new file mode 100644 index 000000000..04fe55aa7 --- /dev/null +++ b/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 +} diff --git a/generated/e8_irrep_tensor_square_decomp/lakefile.toml b/generated/e8_irrep_tensor_square_decomp/lakefile.toml new file mode 100644 index 000000000..e7e0374b9 --- /dev/null +++ b/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" diff --git a/generated/e8_irrep_tensor_square_decomp/lean-toolchain b/generated/e8_irrep_tensor_square_decomp/lean-toolchain new file mode 100644 index 000000000..e7e267fe4 --- /dev/null +++ b/generated/e8_irrep_tensor_square_decomp/lean-toolchain @@ -0,0 +1,2 @@ +leanprover/lean4:v4.30.0-rc1 + diff --git a/generated/exists_complementary_polynomial_on_unit_circle/lakefile.toml b/generated/exists_complementary_polynomial_on_unit_circle/lakefile.toml index 11e592b1c..e14cee101 100644 --- a/generated/exists_complementary_polynomial_on_unit_circle/lakefile.toml +++ b/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" diff --git a/generated/finite_graph_ramsey_theorem/lakefile.toml b/generated/finite_graph_ramsey_theorem/lakefile.toml index f6f803c32..966bb6480 100644 --- a/generated/finite_graph_ramsey_theorem/lakefile.toml +++ b/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" diff --git a/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/lakefile.toml b/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/lakefile.toml index 2b6d77827..03702ebf9 100644 --- a/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/lakefile.toml +++ b/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" diff --git a/generated/g2_irrep_tensor_square_decomp/Challenge.lean b/generated/g2_irrep_tensor_square_decomp/Challenge.lean new file mode 100644 index 000000000..c5dc967d7 --- /dev/null +++ b/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 diff --git a/generated/g2_irrep_tensor_square_decomp/ChallengeDeps.lean b/generated/g2_irrep_tensor_square_decomp/ChallengeDeps.lean new file mode 100644 index 000000000..9952fda9b --- /dev/null +++ b/generated/g2_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 diff --git a/generated/g2_irrep_tensor_square_decomp/README.md b/generated/g2_irrep_tensor_square_decomp/README.md new file mode 100644 index 000000000..63c199df0 --- /dev/null +++ b/generated/g2_irrep_tensor_square_decomp/README.md @@ -0,0 +1,25 @@ +# `g2_irrep_tensor_square_decomp` + +Tensor square decomposition of a 64-dim irreducible g₂-representation + +- Problem ID: `g2_irrep_tensor_square_decomp` +- Test Problem: no +- Submitter: Kim Morrison +- Notes: g₂ is the smallest exceptional Lie algebra, defined here by the Serre construction (Mathlib's `LieAlgebra.g₂`). The relevant irreducible representation has highest weight ω₁ + ω₂ (the sum of the two fundamental weights), dimension 64; its tensor square decomposes into 14 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 g₂. +- Informal solution: Construct V as the irreducible 64-dim representation V(ω₁+ω₂). Decomposition (LiE-verified): V⊗V = V(0,0) + V(1,0) + 2V(0,1) + 2V(2,0) + 2V(1,1) + 2V(0,2) + 3V(3,0) + 3V(2,1) + V(1,2) + V(0,3) + 2V(4,0) + 2V(3,1) + V(2,2) + V(5,0). The 14 distinct highest weights give 14 isotypic components. + +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. diff --git a/generated/g2_irrep_tensor_square_decomp/Solution.lean b/generated/g2_irrep_tensor_square_decomp/Solution.lean new file mode 100644 index 000000000..f82397c68 --- /dev/null +++ b/generated/g2_irrep_tensor_square_decomp/Solution.lean @@ -0,0 +1,14 @@ +import ChallengeDeps +import Submission + +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 + exact Submission.g2_irrep_tensor_square_decomp diff --git a/generated/g2_irrep_tensor_square_decomp/Submission.lean b/generated/g2_irrep_tensor_square_decomp/Submission.lean new file mode 100644 index 000000000..048a27569 --- /dev/null +++ b/generated/g2_irrep_tensor_square_decomp/Submission.lean @@ -0,0 +1,18 @@ +import ChallengeDeps +import Submission.Helpers + +open LeanEval.RepresentationTheory +open scoped TensorProduct + +namespace Submission + +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 + +end Submission diff --git a/generated/g2_irrep_tensor_square_decomp/Submission/Helpers.lean b/generated/g2_irrep_tensor_square_decomp/Submission/Helpers.lean new file mode 100644 index 000000000..1561e7c8a --- /dev/null +++ b/generated/g2_irrep_tensor_square_decomp/Submission/Helpers.lean @@ -0,0 +1,3 @@ +namespace Submission.Helpers + +end Submission.Helpers diff --git a/generated/g2_irrep_tensor_square_decomp/WorkspaceTest.lean b/generated/g2_irrep_tensor_square_decomp/WorkspaceTest.lean new file mode 100644 index 000000000..ecb65777d --- /dev/null +++ b/generated/g2_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 diff --git a/generated/g2_irrep_tensor_square_decomp/config.json b/generated/g2_irrep_tensor_square_decomp/config.json new file mode 100644 index 000000000..2ab3e5034 --- /dev/null +++ b/generated/g2_irrep_tensor_square_decomp/config.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": [ + "g2_irrep_tensor_square_decomp" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": false +} diff --git a/generated/g2_irrep_tensor_square_decomp/lakefile.toml b/generated/g2_irrep_tensor_square_decomp/lakefile.toml new file mode 100644 index 000000000..24874c07f --- /dev/null +++ b/generated/g2_irrep_tensor_square_decomp/lakefile.toml @@ -0,0 +1,27 @@ +name = "g2_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" diff --git a/generated/g2_irrep_tensor_square_decomp/lean-toolchain b/generated/g2_irrep_tensor_square_decomp/lean-toolchain new file mode 100644 index 000000000..e7e267fe4 --- /dev/null +++ b/generated/g2_irrep_tensor_square_decomp/lean-toolchain @@ -0,0 +1,2 @@ +leanprover/lean4:v4.30.0-rc1 + diff --git a/generated/glAction_range_eq_centralizer_symAction/Challenge.lean b/generated/glAction_range_eq_centralizer_symAction/Challenge.lean new file mode 100644 index 000000000..82e14d747 --- /dev/null +++ b/generated/glAction_range_eq_centralizer_symAction/Challenge.lean @@ -0,0 +1,11 @@ +import ChallengeDeps + +open LeanEval.RepresentationTheory +open scoped TensorProduct + +theorem glAction_range_eq_centralizer_symAction {R : Type*} [Field R] + {M : Type*} [AddCommGroup M] [Module R M] [FiniteDimensional R M] + {k : ℕ} [Invertible (k.factorial : R)] : + Algebra.adjoin R (Set.range (glAction R M k)) = + Subalgebra.centralizer R (Set.range (symAction R M k)) := by + sorry diff --git a/generated/glAction_range_eq_centralizer_symAction/ChallengeDeps.lean b/generated/glAction_range_eq_centralizer_symAction/ChallengeDeps.lean new file mode 100644 index 000000000..77e001c34 --- /dev/null +++ b/generated/glAction_range_eq_centralizer_symAction/ChallengeDeps.lean @@ -0,0 +1,47 @@ +import Mathlib + +namespace LeanEval +namespace RepresentationTheory + +open scoped TensorProduct + +/-! +Schur–Weyl duality on `V^⊗k`. + +Two commuting actions on `V^⊗k`: + +* `symAction`: the symmetric group `S_k` acts by permuting tensor factors. +* `glAction`: the general linear group `GL(V)` acts diagonally as `g · (v₁ ⊗ ⋯ ⊗ v_k) = + (g v₁) ⊗ ⋯ ⊗ (g v_k)`. + +Schur–Weyl duality says their images in `End(V^⊗k)` generate mutual centralizers. We state +the two directions as separate `eval_problem`s. +-/ + +/-- The symmetric group `S_k` acts on `V^⊗k` by permuting the tensor factors. -/ +def symAction (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M] (k : ℕ) : + Equiv.Perm (Fin k) →* Module.End R (⨂[R]^k M) where + toFun σ := (PiTensorProduct.reindex R (fun _ : Fin k => M) σ).toLinearMap + map_one' := by + ext x + simp only [LinearEquiv.coe_coe, LinearMap.coe_compMultilinearMap, Function.comp_apply, + PiTensorProduct.reindex_tprod, Module.End.one_apply] + rfl + map_mul' σ τ := by + ext x + simp only [Module.End.mul_apply, LinearEquiv.coe_coe, LinearMap.coe_compMultilinearMap, + Function.comp_apply, PiTensorProduct.reindex_tprod] + rfl + +/-- The general linear group `GL(V)` acts diagonally on `V^⊗k`: +`g · (v₁ ⊗ ⋯ ⊗ v_k) = (g v₁) ⊗ ⋯ ⊗ (g v_k)`. -/ +def glAction (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M] (k : ℕ) : + (M →ₗ[R] M)ˣ →* Module.End R (⨂[R]^k M) where + toFun g := PiTensorProduct.map (fun _ : Fin k => (g : M →ₗ[R] M)) + map_one' := by ext x; simp + map_mul' g h := by ext x; simp + + + +end RepresentationTheory +end LeanEval diff --git a/generated/glAction_range_eq_centralizer_symAction/README.md b/generated/glAction_range_eq_centralizer_symAction/README.md new file mode 100644 index 000000000..6c61c04b4 --- /dev/null +++ b/generated/glAction_range_eq_centralizer_symAction/README.md @@ -0,0 +1,25 @@ +# `glAction_range_eq_centralizer_symAction` + +Schur-Weyl duality: GL(V) image equals centralizer of S_k image + +- Problem ID: `glAction_range_eq_centralizer_symAction` +- Test Problem: no +- Submitter: Kim Morrison +- Notes: The other direction of Schur-Weyl duality: the subalgebra of End(V^⊗k) generated by the diagonal GL(V) action equals the centralizer of the subalgebra generated by the S_k action. +- Source: H. Weyl, The Classical Groups, 1939; I. Schur, Über die rationalen Darstellungen der allgemeinen linearen Gruppe, 1927. +- Informal solution: By polarization over R with k! invertible, the subalgebra generated by {g^⊗k : g ∈ GL(V)} is precisely the image of Sym^k(End V), i.e., the endomorphisms of V^⊗k fixed by the S_k-action on tensor factors of End V. An endomorphism of V^⊗k fixed by this action is exactly one commuting with the S_k action on V^⊗k. + +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. diff --git a/generated/glAction_range_eq_centralizer_symAction/Solution.lean b/generated/glAction_range_eq_centralizer_symAction/Solution.lean new file mode 100644 index 000000000..a72fd4cbd --- /dev/null +++ b/generated/glAction_range_eq_centralizer_symAction/Solution.lean @@ -0,0 +1,12 @@ +import ChallengeDeps +import Submission + +open LeanEval.RepresentationTheory +open scoped TensorProduct + +theorem glAction_range_eq_centralizer_symAction {R : Type*} [Field R] + {M : Type*} [AddCommGroup M] [Module R M] [FiniteDimensional R M] + {k : ℕ} [Invertible (k.factorial : R)] : + Algebra.adjoin R (Set.range (glAction R M k)) = + Subalgebra.centralizer R (Set.range (symAction R M k)) := by + exact Submission.glAction_range_eq_centralizer_symAction diff --git a/generated/glAction_range_eq_centralizer_symAction/Submission.lean b/generated/glAction_range_eq_centralizer_symAction/Submission.lean new file mode 100644 index 000000000..c9ad34bac --- /dev/null +++ b/generated/glAction_range_eq_centralizer_symAction/Submission.lean @@ -0,0 +1,16 @@ +import ChallengeDeps +import Submission.Helpers + +open LeanEval.RepresentationTheory +open scoped TensorProduct + +namespace Submission + +theorem glAction_range_eq_centralizer_symAction {R : Type*} [Field R] + {M : Type*} [AddCommGroup M] [Module R M] [FiniteDimensional R M] + {k : ℕ} [Invertible (k.factorial : R)] : + Algebra.adjoin R (Set.range (glAction R M k)) = + Subalgebra.centralizer R (Set.range (symAction R M k)) := by + sorry + +end Submission diff --git a/generated/glAction_range_eq_centralizer_symAction/Submission/Helpers.lean b/generated/glAction_range_eq_centralizer_symAction/Submission/Helpers.lean new file mode 100644 index 000000000..1561e7c8a --- /dev/null +++ b/generated/glAction_range_eq_centralizer_symAction/Submission/Helpers.lean @@ -0,0 +1,3 @@ +namespace Submission.Helpers + +end Submission.Helpers diff --git a/generated/glAction_range_eq_centralizer_symAction/WorkspaceTest.lean b/generated/glAction_range_eq_centralizer_symAction/WorkspaceTest.lean new file mode 100644 index 000000000..ecb65777d --- /dev/null +++ b/generated/glAction_range_eq_centralizer_symAction/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 diff --git a/generated/glAction_range_eq_centralizer_symAction/config.json b/generated/glAction_range_eq_centralizer_symAction/config.json new file mode 100644 index 000000000..1f70b572f --- /dev/null +++ b/generated/glAction_range_eq_centralizer_symAction/config.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": [ + "glAction_range_eq_centralizer_symAction" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": false +} diff --git a/generated/glAction_range_eq_centralizer_symAction/lakefile.toml b/generated/glAction_range_eq_centralizer_symAction/lakefile.toml new file mode 100644 index 000000000..9a0d80c20 --- /dev/null +++ b/generated/glAction_range_eq_centralizer_symAction/lakefile.toml @@ -0,0 +1,27 @@ +name = "glAction_range_eq_centralizer_symAction" +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" diff --git a/generated/glAction_range_eq_centralizer_symAction/lean-toolchain b/generated/glAction_range_eq_centralizer_symAction/lean-toolchain new file mode 100644 index 000000000..e7e267fe4 --- /dev/null +++ b/generated/glAction_range_eq_centralizer_symAction/lean-toolchain @@ -0,0 +1,2 @@ +leanprover/lean4:v4.30.0-rc1 + diff --git a/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/lakefile.toml b/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/lakefile.toml index 06d4b505f..b74414df6 100644 --- a/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/lakefile.toml +++ b/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/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" diff --git a/generated/isStarNormal_mul_of_commute/Challenge.lean b/generated/isStarNormal_mul_of_commute/Challenge.lean new file mode 100644 index 000000000..e76f6e54d --- /dev/null +++ b/generated/isStarNormal_mul_of_commute/Challenge.lean @@ -0,0 +1,7 @@ +import Mathlib + +theorem isStarNormal_mul_of_commute {A : Type*} [NonUnitalCStarAlgebra A] + {a b : A} (ha : IsStarNormal a) (hb : IsStarNormal b) + (hab : Commute a b) : + IsStarNormal (a * b) := by + sorry diff --git a/generated/isStarNormal_mul_of_commute/README.md b/generated/isStarNormal_mul_of_commute/README.md new file mode 100644 index 000000000..9259a4ef2 --- /dev/null +++ b/generated/isStarNormal_mul_of_commute/README.md @@ -0,0 +1,25 @@ +# `isStarNormal_mul_of_commute` + +Product of commuting normal elements is normal + +- Problem ID: `isStarNormal_mul_of_commute` +- Test Problem: no +- Submitter: Kim Morrison +- Notes: Uses the Fuglede-Putnam-Rosenblum theorem to show all four of a, star a, b, star b pairwise commute, then verifies the normality condition by direct computation. +- Source: B. Fuglede, A commutativity theorem for normal operators, 1950. +- Informal solution: From Commute a b and normality, apply Fuglede-Putnam twice to get Commute (star a) b and Commute (star a) (star b). Then star(ab)·(ab) = b*·a*·a·b = b*·a·a*·b (a normal) = a·b*·b·a* (all commute) = a·b·b*·a* (b normal) = (ab)·star(ab). + +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. diff --git a/generated/isStarNormal_mul_of_commute/Solution.lean b/generated/isStarNormal_mul_of_commute/Solution.lean new file mode 100644 index 000000000..d9cbd15f0 --- /dev/null +++ b/generated/isStarNormal_mul_of_commute/Solution.lean @@ -0,0 +1,8 @@ +import Mathlib +import Submission + +theorem isStarNormal_mul_of_commute {A : Type*} [NonUnitalCStarAlgebra A] + {a b : A} (ha : IsStarNormal a) (hb : IsStarNormal b) + (hab : Commute a b) : + IsStarNormal (a * b) := by + exact Submission.isStarNormal_mul_of_commute ha hb hab diff --git a/generated/isStarNormal_mul_of_commute/Submission.lean b/generated/isStarNormal_mul_of_commute/Submission.lean new file mode 100644 index 000000000..7aba83b5b --- /dev/null +++ b/generated/isStarNormal_mul_of_commute/Submission.lean @@ -0,0 +1,12 @@ +import Mathlib +import Submission.Helpers + +namespace Submission + +theorem isStarNormal_mul_of_commute {A : Type*} [NonUnitalCStarAlgebra A] + {a b : A} (ha : IsStarNormal a) (hb : IsStarNormal b) + (hab : Commute a b) : + IsStarNormal (a * b) := by + sorry + +end Submission diff --git a/generated/isStarNormal_mul_of_commute/Submission/Helpers.lean b/generated/isStarNormal_mul_of_commute/Submission/Helpers.lean new file mode 100644 index 000000000..1561e7c8a --- /dev/null +++ b/generated/isStarNormal_mul_of_commute/Submission/Helpers.lean @@ -0,0 +1,3 @@ +namespace Submission.Helpers + +end Submission.Helpers diff --git a/generated/isStarNormal_mul_of_commute/WorkspaceTest.lean b/generated/isStarNormal_mul_of_commute/WorkspaceTest.lean new file mode 100644 index 000000000..ecb65777d --- /dev/null +++ b/generated/isStarNormal_mul_of_commute/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 diff --git a/generated/isStarNormal_mul_of_commute/config.json b/generated/isStarNormal_mul_of_commute/config.json new file mode 100644 index 000000000..978900071 --- /dev/null +++ b/generated/isStarNormal_mul_of_commute/config.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": [ + "isStarNormal_mul_of_commute" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": false +} diff --git a/generated/isStarNormal_mul_of_commute/lakefile.toml b/generated/isStarNormal_mul_of_commute/lakefile.toml new file mode 100644 index 000000000..151f5eae8 --- /dev/null +++ b/generated/isStarNormal_mul_of_commute/lakefile.toml @@ -0,0 +1,24 @@ +name = "isStarNormal_mul_of_commute" +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 = "Challenge" + +[[lean_lib]] +name = "Solution" + +[[lean_lib]] +name = "Submission" + +[[lean_exe]] +name = "workspace_test" +root = "WorkspaceTest" diff --git a/generated/isStarNormal_mul_of_commute/lean-toolchain b/generated/isStarNormal_mul_of_commute/lean-toolchain new file mode 100644 index 000000000..e7e267fe4 --- /dev/null +++ b/generated/isStarNormal_mul_of_commute/lean-toolchain @@ -0,0 +1,2 @@ +leanprover/lean4:v4.30.0-rc1 + diff --git a/generated/list_append_singleton_length/lakefile.toml b/generated/list_append_singleton_length/lakefile.toml index 6dcbe7a25..04f512d41 100644 --- a/generated/list_append_singleton_length/lakefile.toml +++ b/generated/list_append_singleton_length/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" diff --git a/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/lakefile.toml b/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/lakefile.toml index 2e7403f08..a3d0e6821 100644 --- a/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/lakefile.toml +++ b/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/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" diff --git a/generated/mulCayley_connected_iff_closure_eq_top/Challenge.lean b/generated/mulCayley_connected_iff_closure_eq_top/Challenge.lean new file mode 100644 index 000000000..a86cecdba --- /dev/null +++ b/generated/mulCayley_connected_iff_closure_eq_top/Challenge.lean @@ -0,0 +1,6 @@ +import Mathlib + +theorem mulCayley_connected_iff_closure_eq_top {G : Type*} [Group G] + (S : Set G) : + (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ := by + sorry diff --git a/generated/mulCayley_connected_iff_closure_eq_top/README.md b/generated/mulCayley_connected_iff_closure_eq_top/README.md new file mode 100644 index 000000000..418aead0f --- /dev/null +++ b/generated/mulCayley_connected_iff_closure_eq_top/README.md @@ -0,0 +1,25 @@ +# `mulCayley_connected_iff_closure_eq_top` + +Cayley graph connected iff generators generate the group + +- Problem ID: `mulCayley_connected_iff_closure_eq_top` +- Test Problem: no +- Submitter: Kim Morrison +- Notes: A foundational result in geometric group theory using the newly defined Cayley graph. Connectivity of the Cayley graph is equivalent to the generating set S generating G as a group. +- Source: A. Cayley, On the theory of groups, as depending on the symbolic equation θ^n = 1, 1878. +- Informal solution: Forward: if connected, any g ∈ G is reached from 1 by a path, which corresponds to a product of generators. Reverse: if S generates, any g is a product of generators, giving a path from 1 to g. + +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. diff --git a/generated/mulCayley_connected_iff_closure_eq_top/Solution.lean b/generated/mulCayley_connected_iff_closure_eq_top/Solution.lean new file mode 100644 index 000000000..61b86c3f3 --- /dev/null +++ b/generated/mulCayley_connected_iff_closure_eq_top/Solution.lean @@ -0,0 +1,7 @@ +import Mathlib +import Submission + +theorem mulCayley_connected_iff_closure_eq_top {G : Type*} [Group G] + (S : Set G) : + (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ := by + exact Submission.mulCayley_connected_iff_closure_eq_top S diff --git a/generated/mulCayley_connected_iff_closure_eq_top/Submission.lean b/generated/mulCayley_connected_iff_closure_eq_top/Submission.lean new file mode 100644 index 000000000..2378fe778 --- /dev/null +++ b/generated/mulCayley_connected_iff_closure_eq_top/Submission.lean @@ -0,0 +1,11 @@ +import Mathlib +import Submission.Helpers + +namespace Submission + +theorem mulCayley_connected_iff_closure_eq_top {G : Type*} [Group G] + (S : Set G) : + (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ := by + sorry + +end Submission diff --git a/generated/mulCayley_connected_iff_closure_eq_top/Submission/Helpers.lean b/generated/mulCayley_connected_iff_closure_eq_top/Submission/Helpers.lean new file mode 100644 index 000000000..1561e7c8a --- /dev/null +++ b/generated/mulCayley_connected_iff_closure_eq_top/Submission/Helpers.lean @@ -0,0 +1,3 @@ +namespace Submission.Helpers + +end Submission.Helpers diff --git a/generated/mulCayley_connected_iff_closure_eq_top/WorkspaceTest.lean b/generated/mulCayley_connected_iff_closure_eq_top/WorkspaceTest.lean new file mode 100644 index 000000000..ecb65777d --- /dev/null +++ b/generated/mulCayley_connected_iff_closure_eq_top/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 diff --git a/generated/mulCayley_connected_iff_closure_eq_top/config.json b/generated/mulCayley_connected_iff_closure_eq_top/config.json new file mode 100644 index 000000000..463bb1384 --- /dev/null +++ b/generated/mulCayley_connected_iff_closure_eq_top/config.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": [ + "mulCayley_connected_iff_closure_eq_top" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": false +} diff --git a/generated/mulCayley_connected_iff_closure_eq_top/lakefile.toml b/generated/mulCayley_connected_iff_closure_eq_top/lakefile.toml new file mode 100644 index 000000000..f38c3fa99 --- /dev/null +++ b/generated/mulCayley_connected_iff_closure_eq_top/lakefile.toml @@ -0,0 +1,24 @@ +name = "mulCayley_connected_iff_closure_eq_top" +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 = "Challenge" + +[[lean_lib]] +name = "Solution" + +[[lean_lib]] +name = "Submission" + +[[lean_exe]] +name = "workspace_test" +root = "WorkspaceTest" diff --git a/generated/mulCayley_connected_iff_closure_eq_top/lean-toolchain b/generated/mulCayley_connected_iff_closure_eq_top/lean-toolchain new file mode 100644 index 000000000..e7e267fe4 --- /dev/null +++ b/generated/mulCayley_connected_iff_closure_eq_top/lean-toolchain @@ -0,0 +1,2 @@ +leanprover/lean4:v4.30.0-rc1 + diff --git a/generated/oppenheim_inequality/Challenge.lean b/generated/oppenheim_inequality/Challenge.lean new file mode 100644 index 000000000..e4d19d667 --- /dev/null +++ b/generated/oppenheim_inequality/Challenge.lean @@ -0,0 +1,8 @@ +import Mathlib + +open scoped MatrixOrder Matrix + +theorem oppenheim_inequality {n : Type*} [Fintype n] [DecidableEq n] + {A B : Matrix n n ℝ} (hA : A.PosSemidef) (hB : B.PosSemidef) : + A.det * ∏ i, B i i ≤ (A ⊙ B).det := by + sorry diff --git a/generated/oppenheim_inequality/README.md b/generated/oppenheim_inequality/README.md new file mode 100644 index 000000000..09adf5132 --- /dev/null +++ b/generated/oppenheim_inequality/README.md @@ -0,0 +1,25 @@ +# `oppenheim_inequality` + +Oppenheim's inequality for Hadamard products + +- Problem ID: `oppenheim_inequality` +- Test Problem: no +- Submitter: Kim Morrison +- Notes: Oppenheim's 1930 inequality: for PSD matrices A, B, det(A ⊙ B) ≥ det(A) · ∏ᵢ Bᵢᵢ. Uses the Schur product theorem (newly formalized) as a key ingredient. +- Source: I. Schur, Bemerkungen zur Theorie der beschränkten Bilinearformen, 1911; A. Oppenheim, Inequalities connected with definite Hermitian forms, 1930. +- Informal solution: Use induction on the matrix size, extracting a Schur complement at each step and applying the Schur product theorem to bound the determinant. + +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. diff --git a/generated/oppenheim_inequality/Solution.lean b/generated/oppenheim_inequality/Solution.lean new file mode 100644 index 000000000..94efeec9f --- /dev/null +++ b/generated/oppenheim_inequality/Solution.lean @@ -0,0 +1,9 @@ +import Mathlib +import Submission + +open scoped MatrixOrder Matrix + +theorem oppenheim_inequality {n : Type*} [Fintype n] [DecidableEq n] + {A B : Matrix n n ℝ} (hA : A.PosSemidef) (hB : B.PosSemidef) : + A.det * ∏ i, B i i ≤ (A ⊙ B).det := by + exact Submission.oppenheim_inequality hA hB diff --git a/generated/oppenheim_inequality/Submission.lean b/generated/oppenheim_inequality/Submission.lean new file mode 100644 index 000000000..28f41c666 --- /dev/null +++ b/generated/oppenheim_inequality/Submission.lean @@ -0,0 +1,13 @@ +import Mathlib +import Submission.Helpers + +open scoped MatrixOrder Matrix + +namespace Submission + +theorem oppenheim_inequality {n : Type*} [Fintype n] [DecidableEq n] + {A B : Matrix n n ℝ} (hA : A.PosSemidef) (hB : B.PosSemidef) : + A.det * ∏ i, B i i ≤ (A ⊙ B).det := by + sorry + +end Submission diff --git a/generated/oppenheim_inequality/Submission/Helpers.lean b/generated/oppenheim_inequality/Submission/Helpers.lean new file mode 100644 index 000000000..1561e7c8a --- /dev/null +++ b/generated/oppenheim_inequality/Submission/Helpers.lean @@ -0,0 +1,3 @@ +namespace Submission.Helpers + +end Submission.Helpers diff --git a/generated/oppenheim_inequality/WorkspaceTest.lean b/generated/oppenheim_inequality/WorkspaceTest.lean new file mode 100644 index 000000000..ecb65777d --- /dev/null +++ b/generated/oppenheim_inequality/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 diff --git a/generated/oppenheim_inequality/config.json b/generated/oppenheim_inequality/config.json new file mode 100644 index 000000000..1117ee069 --- /dev/null +++ b/generated/oppenheim_inequality/config.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": [ + "oppenheim_inequality" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": false +} diff --git a/generated/oppenheim_inequality/lakefile.toml b/generated/oppenheim_inequality/lakefile.toml new file mode 100644 index 000000000..02c7f1666 --- /dev/null +++ b/generated/oppenheim_inequality/lakefile.toml @@ -0,0 +1,24 @@ +name = "oppenheim_inequality" +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 = "Challenge" + +[[lean_lib]] +name = "Solution" + +[[lean_lib]] +name = "Submission" + +[[lean_exe]] +name = "workspace_test" +root = "WorkspaceTest" diff --git a/generated/oppenheim_inequality/lean-toolchain b/generated/oppenheim_inequality/lean-toolchain new file mode 100644 index 000000000..e7e267fe4 --- /dev/null +++ b/generated/oppenheim_inequality/lean-toolchain @@ -0,0 +1,2 @@ +leanprover/lean4:v4.30.0-rc1 + diff --git a/generated/posSemidef_map_exp/Challenge.lean b/generated/posSemidef_map_exp/Challenge.lean new file mode 100644 index 000000000..0c585f3e1 --- /dev/null +++ b/generated/posSemidef_map_exp/Challenge.lean @@ -0,0 +1,8 @@ +import Mathlib + +open scoped MatrixOrder Matrix + +theorem posSemidef_map_exp {n : Type*} [Fintype n] [DecidableEq n] + {A : Matrix n n ℝ} (hA : A.PosSemidef) : + (A.map Real.exp).PosSemidef := by + sorry diff --git a/generated/posSemidef_map_exp/README.md b/generated/posSemidef_map_exp/README.md new file mode 100644 index 000000000..cc1179c5b --- /dev/null +++ b/generated/posSemidef_map_exp/README.md @@ -0,0 +1,25 @@ +# `posSemidef_map_exp` + +Entrywise exponential of a PSD matrix is PSD + +- Problem ID: `posSemidef_map_exp` +- Test Problem: no +- Submitter: Kim Morrison +- Notes: Part of the Schur-Polya-Loewner theory of entrywise functions preserving PSD. The proof uses the Schur product theorem iteratively: exp_⊙(A) = ∑ A^{⊙k}/k!, each Hadamard power is PSD, and the convergent series of PSD matrices is PSD. +- Source: I.J. Schoenberg, Positive definite functions on spheres, 1942. +- Informal solution: Write exp(a_{ij}) as the convergent series ∑ (a_{ij})^k / k!. The matrix with entries (a_{ij})^k is the k-fold Hadamard product A^{⊙k}, which is PSD by iterated Schur product. The partial sums are nonneg combinations of PSD matrices, hence PSD. PSD is a closed condition, so the limit is PSD. + +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. diff --git a/generated/posSemidef_map_exp/Solution.lean b/generated/posSemidef_map_exp/Solution.lean new file mode 100644 index 000000000..9acb23ac6 --- /dev/null +++ b/generated/posSemidef_map_exp/Solution.lean @@ -0,0 +1,9 @@ +import Mathlib +import Submission + +open scoped MatrixOrder Matrix + +theorem posSemidef_map_exp {n : Type*} [Fintype n] [DecidableEq n] + {A : Matrix n n ℝ} (hA : A.PosSemidef) : + (A.map Real.exp).PosSemidef := by + exact Submission.posSemidef_map_exp hA diff --git a/generated/posSemidef_map_exp/Submission.lean b/generated/posSemidef_map_exp/Submission.lean new file mode 100644 index 000000000..b69269711 --- /dev/null +++ b/generated/posSemidef_map_exp/Submission.lean @@ -0,0 +1,13 @@ +import Mathlib +import Submission.Helpers + +open scoped MatrixOrder Matrix + +namespace Submission + +theorem posSemidef_map_exp {n : Type*} [Fintype n] [DecidableEq n] + {A : Matrix n n ℝ} (hA : A.PosSemidef) : + (A.map Real.exp).PosSemidef := by + sorry + +end Submission diff --git a/generated/posSemidef_map_exp/Submission/Helpers.lean b/generated/posSemidef_map_exp/Submission/Helpers.lean new file mode 100644 index 000000000..1561e7c8a --- /dev/null +++ b/generated/posSemidef_map_exp/Submission/Helpers.lean @@ -0,0 +1,3 @@ +namespace Submission.Helpers + +end Submission.Helpers diff --git a/generated/posSemidef_map_exp/WorkspaceTest.lean b/generated/posSemidef_map_exp/WorkspaceTest.lean new file mode 100644 index 000000000..ecb65777d --- /dev/null +++ b/generated/posSemidef_map_exp/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 diff --git a/generated/posSemidef_map_exp/config.json b/generated/posSemidef_map_exp/config.json new file mode 100644 index 000000000..a6a212295 --- /dev/null +++ b/generated/posSemidef_map_exp/config.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": [ + "posSemidef_map_exp" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": false +} diff --git a/generated/posSemidef_map_exp/lakefile.toml b/generated/posSemidef_map_exp/lakefile.toml new file mode 100644 index 000000000..5bc45da3c --- /dev/null +++ b/generated/posSemidef_map_exp/lakefile.toml @@ -0,0 +1,24 @@ +name = "posSemidef_map_exp" +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 = "Challenge" + +[[lean_lib]] +name = "Solution" + +[[lean_lib]] +name = "Submission" + +[[lean_exe]] +name = "workspace_test" +root = "WorkspaceTest" diff --git a/generated/posSemidef_map_exp/lean-toolchain b/generated/posSemidef_map_exp/lean-toolchain new file mode 100644 index 000000000..e7e267fe4 --- /dev/null +++ b/generated/posSemidef_map_exp/lean-toolchain @@ -0,0 +1,2 @@ +leanprover/lean4:v4.30.0-rc1 + diff --git a/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/Challenge.lean b/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/Challenge.lean index 72a4aa0f6..df5c53780 100644 --- a/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/Challenge.lean +++ b/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/Challenge.lean @@ -1,5 +1,6 @@ import ChallengeDeps +open LeanEval.NumberTheory open scoped ArithmeticFunction.sigma theorem riemann_hypothesis_iff_lagarias_elementary_criterion : diff --git a/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/Solution.lean b/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/Solution.lean index 0c5057fea..d55d8c8a6 100644 --- a/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/Solution.lean +++ b/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/Solution.lean @@ -1,6 +1,7 @@ import ChallengeDeps import Submission +open LeanEval.NumberTheory open scoped ArithmeticFunction.sigma theorem riemann_hypothesis_iff_lagarias_elementary_criterion : diff --git a/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/Submission.lean b/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/Submission.lean index 8adbc0e94..f32fc055f 100644 --- a/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/Submission.lean +++ b/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/Submission.lean @@ -1,6 +1,7 @@ import ChallengeDeps import Submission.Helpers +open LeanEval.NumberTheory open scoped ArithmeticFunction.sigma namespace Submission diff --git a/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/lakefile.toml b/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/lakefile.toml index b81f16289..a3969ac92 100644 --- a/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/lakefile.toml +++ b/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/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" diff --git a/generated/rouche_logCounting_zero_eq/lakefile.toml b/generated/rouche_logCounting_zero_eq/lakefile.toml index cea4a8790..2fe104470 100644 --- a/generated/rouche_logCounting_zero_eq/lakefile.toml +++ b/generated/rouche_logCounting_zero_eq/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" diff --git a/generated/substInv_X_sub_X_sq_eq_catalan/Challenge.lean b/generated/substInv_X_sub_X_sq_eq_catalan/Challenge.lean new file mode 100644 index 000000000..2321474ef --- /dev/null +++ b/generated/substInv_X_sub_X_sq_eq_catalan/Challenge.lean @@ -0,0 +1,10 @@ +import Mathlib + +open PowerSeries + +theorem substInv_X_sub_X_sq_eq_catalan (n : ℕ) : + haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := by + simp [coeff_X, coeff_X_pow]; exact invertibleOne + coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) = + (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := by + sorry diff --git a/generated/substInv_X_sub_X_sq_eq_catalan/README.md b/generated/substInv_X_sub_X_sq_eq_catalan/README.md new file mode 100644 index 000000000..80dd1ae3a --- /dev/null +++ b/generated/substInv_X_sub_X_sq_eq_catalan/README.md @@ -0,0 +1,25 @@ +# `substInv_X_sub_X_sq_eq_catalan` + +Catalan generating function via compositional inversion + +- Problem ID: `substInv_X_sub_X_sq_eq_catalan` +- Test Problem: no +- Submitter: Kim Morrison +- Notes: The compositional inverse of X - X² is the generating function for Catalan numbers. This is a classical application of Lagrange inversion in enumerative combinatorics, connecting formal power series inversion to Dyck paths, binary trees, and triangulations. +- Source: E. Catalan, Note sur une équation aux différences finies, 1838; J.-L. Lagrange, Nouvelle méthode pour résoudre les équations littérales, 1770. +- Informal solution: The compositional inverse C(x) satisfies C - C² = x, giving C = (1 - √(1-4x))/2. By the binomial series, its coefficients are the Catalan numbers C_n = (2n choose n)/(n+1). + +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. diff --git a/generated/substInv_X_sub_X_sq_eq_catalan/Solution.lean b/generated/substInv_X_sub_X_sq_eq_catalan/Solution.lean new file mode 100644 index 000000000..15088247f --- /dev/null +++ b/generated/substInv_X_sub_X_sq_eq_catalan/Solution.lean @@ -0,0 +1,11 @@ +import Mathlib +import Submission + +open PowerSeries + +theorem substInv_X_sub_X_sq_eq_catalan (n : ℕ) : + haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := by + simp [coeff_X, coeff_X_pow]; exact invertibleOne + coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) = + (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := by + exact Submission.substInv_X_sub_X_sq_eq_catalan n diff --git a/generated/substInv_X_sub_X_sq_eq_catalan/Submission.lean b/generated/substInv_X_sub_X_sq_eq_catalan/Submission.lean new file mode 100644 index 000000000..0a72f81f9 --- /dev/null +++ b/generated/substInv_X_sub_X_sq_eq_catalan/Submission.lean @@ -0,0 +1,15 @@ +import Mathlib +import Submission.Helpers + +open PowerSeries + +namespace Submission + +theorem substInv_X_sub_X_sq_eq_catalan (n : ℕ) : + haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := by + simp [coeff_X, coeff_X_pow]; exact invertibleOne + coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) = + (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := by + sorry + +end Submission diff --git a/generated/substInv_X_sub_X_sq_eq_catalan/Submission/Helpers.lean b/generated/substInv_X_sub_X_sq_eq_catalan/Submission/Helpers.lean new file mode 100644 index 000000000..1561e7c8a --- /dev/null +++ b/generated/substInv_X_sub_X_sq_eq_catalan/Submission/Helpers.lean @@ -0,0 +1,3 @@ +namespace Submission.Helpers + +end Submission.Helpers diff --git a/generated/substInv_X_sub_X_sq_eq_catalan/WorkspaceTest.lean b/generated/substInv_X_sub_X_sq_eq_catalan/WorkspaceTest.lean new file mode 100644 index 000000000..ecb65777d --- /dev/null +++ b/generated/substInv_X_sub_X_sq_eq_catalan/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 diff --git a/generated/substInv_X_sub_X_sq_eq_catalan/config.json b/generated/substInv_X_sub_X_sq_eq_catalan/config.json new file mode 100644 index 000000000..1593a06e6 --- /dev/null +++ b/generated/substInv_X_sub_X_sq_eq_catalan/config.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": [ + "substInv_X_sub_X_sq_eq_catalan" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": false +} diff --git a/generated/substInv_X_sub_X_sq_eq_catalan/lakefile.toml b/generated/substInv_X_sub_X_sq_eq_catalan/lakefile.toml new file mode 100644 index 000000000..359dda9aa --- /dev/null +++ b/generated/substInv_X_sub_X_sq_eq_catalan/lakefile.toml @@ -0,0 +1,24 @@ +name = "substInv_X_sub_X_sq_eq_catalan" +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 = "Challenge" + +[[lean_lib]] +name = "Solution" + +[[lean_lib]] +name = "Submission" + +[[lean_exe]] +name = "workspace_test" +root = "WorkspaceTest" diff --git a/generated/substInv_X_sub_X_sq_eq_catalan/lean-toolchain b/generated/substInv_X_sub_X_sq_eq_catalan/lean-toolchain new file mode 100644 index 000000000..e7e267fe4 --- /dev/null +++ b/generated/substInv_X_sub_X_sq_eq_catalan/lean-toolchain @@ -0,0 +1,2 @@ +leanprover/lean4:v4.30.0-rc1 + diff --git a/generated/symAction_range_eq_centralizer_glAction/Challenge.lean b/generated/symAction_range_eq_centralizer_glAction/Challenge.lean new file mode 100644 index 000000000..dd3f27873 --- /dev/null +++ b/generated/symAction_range_eq_centralizer_glAction/Challenge.lean @@ -0,0 +1,11 @@ +import ChallengeDeps + +open LeanEval.RepresentationTheory +open scoped TensorProduct + +theorem symAction_range_eq_centralizer_glAction {R : Type*} [Field R] + {M : Type*} [AddCommGroup M] [Module R M] [FiniteDimensional R M] + {k : ℕ} [Invertible (k.factorial : R)] : + Algebra.adjoin R (Set.range (symAction R M k)) = + Subalgebra.centralizer R (Set.range (glAction R M k)) := by + sorry diff --git a/generated/symAction_range_eq_centralizer_glAction/ChallengeDeps.lean b/generated/symAction_range_eq_centralizer_glAction/ChallengeDeps.lean new file mode 100644 index 000000000..77e001c34 --- /dev/null +++ b/generated/symAction_range_eq_centralizer_glAction/ChallengeDeps.lean @@ -0,0 +1,47 @@ +import Mathlib + +namespace LeanEval +namespace RepresentationTheory + +open scoped TensorProduct + +/-! +Schur–Weyl duality on `V^⊗k`. + +Two commuting actions on `V^⊗k`: + +* `symAction`: the symmetric group `S_k` acts by permuting tensor factors. +* `glAction`: the general linear group `GL(V)` acts diagonally as `g · (v₁ ⊗ ⋯ ⊗ v_k) = + (g v₁) ⊗ ⋯ ⊗ (g v_k)`. + +Schur–Weyl duality says their images in `End(V^⊗k)` generate mutual centralizers. We state +the two directions as separate `eval_problem`s. +-/ + +/-- The symmetric group `S_k` acts on `V^⊗k` by permuting the tensor factors. -/ +def symAction (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M] (k : ℕ) : + Equiv.Perm (Fin k) →* Module.End R (⨂[R]^k M) where + toFun σ := (PiTensorProduct.reindex R (fun _ : Fin k => M) σ).toLinearMap + map_one' := by + ext x + simp only [LinearEquiv.coe_coe, LinearMap.coe_compMultilinearMap, Function.comp_apply, + PiTensorProduct.reindex_tprod, Module.End.one_apply] + rfl + map_mul' σ τ := by + ext x + simp only [Module.End.mul_apply, LinearEquiv.coe_coe, LinearMap.coe_compMultilinearMap, + Function.comp_apply, PiTensorProduct.reindex_tprod] + rfl + +/-- The general linear group `GL(V)` acts diagonally on `V^⊗k`: +`g · (v₁ ⊗ ⋯ ⊗ v_k) = (g v₁) ⊗ ⋯ ⊗ (g v_k)`. -/ +def glAction (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M] (k : ℕ) : + (M →ₗ[R] M)ˣ →* Module.End R (⨂[R]^k M) where + toFun g := PiTensorProduct.map (fun _ : Fin k => (g : M →ₗ[R] M)) + map_one' := by ext x; simp + map_mul' g h := by ext x; simp + + + +end RepresentationTheory +end LeanEval diff --git a/generated/symAction_range_eq_centralizer_glAction/README.md b/generated/symAction_range_eq_centralizer_glAction/README.md new file mode 100644 index 000000000..1d62fa420 --- /dev/null +++ b/generated/symAction_range_eq_centralizer_glAction/README.md @@ -0,0 +1,25 @@ +# `symAction_range_eq_centralizer_glAction` + +Schur-Weyl duality: S_k image equals centralizer of GL(V) image + +- Problem ID: `symAction_range_eq_centralizer_glAction` +- Test Problem: no +- Submitter: Kim Morrison +- Notes: One direction of Schur-Weyl duality: the subalgebra of End(V^⊗k) generated by the S_k action (permuting factors) equals the centralizer of the subalgebra generated by the diagonal GL(V) action. Hypothesis `Invertible (k! : R)` over a field is exactly the Maschke condition for R[S_k]. +- Source: H. Weyl, The Classical Groups, 1939; I. Schur, Über die rationalen Darstellungen der allgemeinen linearen Gruppe, 1927. +- Informal solution: Classical proof: any T ∈ End(V^⊗k) commuting with GL(V) acts the same way on tensors related by g^⊗k for every g, and by polarization (which uses k! invertible) the subalgebra {g^⊗k : g ∈ GL(V)} linearly spans the image of Sym^k(End V) in End(V^⊗k). Together with the semisimplicity of R[S_k] (Maschke, from the same k! hypothesis) and double commutant for finite-dimensional semisimple algebras, T lies in the R-subalgebra generated by the S_k action. + +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. diff --git a/generated/symAction_range_eq_centralizer_glAction/Solution.lean b/generated/symAction_range_eq_centralizer_glAction/Solution.lean new file mode 100644 index 000000000..98f5ad0e0 --- /dev/null +++ b/generated/symAction_range_eq_centralizer_glAction/Solution.lean @@ -0,0 +1,12 @@ +import ChallengeDeps +import Submission + +open LeanEval.RepresentationTheory +open scoped TensorProduct + +theorem symAction_range_eq_centralizer_glAction {R : Type*} [Field R] + {M : Type*} [AddCommGroup M] [Module R M] [FiniteDimensional R M] + {k : ℕ} [Invertible (k.factorial : R)] : + Algebra.adjoin R (Set.range (symAction R M k)) = + Subalgebra.centralizer R (Set.range (glAction R M k)) := by + exact Submission.symAction_range_eq_centralizer_glAction diff --git a/generated/symAction_range_eq_centralizer_glAction/Submission.lean b/generated/symAction_range_eq_centralizer_glAction/Submission.lean new file mode 100644 index 000000000..fb54a489b --- /dev/null +++ b/generated/symAction_range_eq_centralizer_glAction/Submission.lean @@ -0,0 +1,16 @@ +import ChallengeDeps +import Submission.Helpers + +open LeanEval.RepresentationTheory +open scoped TensorProduct + +namespace Submission + +theorem symAction_range_eq_centralizer_glAction {R : Type*} [Field R] + {M : Type*} [AddCommGroup M] [Module R M] [FiniteDimensional R M] + {k : ℕ} [Invertible (k.factorial : R)] : + Algebra.adjoin R (Set.range (symAction R M k)) = + Subalgebra.centralizer R (Set.range (glAction R M k)) := by + sorry + +end Submission diff --git a/generated/symAction_range_eq_centralizer_glAction/Submission/Helpers.lean b/generated/symAction_range_eq_centralizer_glAction/Submission/Helpers.lean new file mode 100644 index 000000000..1561e7c8a --- /dev/null +++ b/generated/symAction_range_eq_centralizer_glAction/Submission/Helpers.lean @@ -0,0 +1,3 @@ +namespace Submission.Helpers + +end Submission.Helpers diff --git a/generated/symAction_range_eq_centralizer_glAction/WorkspaceTest.lean b/generated/symAction_range_eq_centralizer_glAction/WorkspaceTest.lean new file mode 100644 index 000000000..ecb65777d --- /dev/null +++ b/generated/symAction_range_eq_centralizer_glAction/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 diff --git a/generated/symAction_range_eq_centralizer_glAction/config.json b/generated/symAction_range_eq_centralizer_glAction/config.json new file mode 100644 index 000000000..1adf95688 --- /dev/null +++ b/generated/symAction_range_eq_centralizer_glAction/config.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": [ + "symAction_range_eq_centralizer_glAction" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": false +} diff --git a/generated/symAction_range_eq_centralizer_glAction/lakefile.toml b/generated/symAction_range_eq_centralizer_glAction/lakefile.toml new file mode 100644 index 000000000..0e7093b68 --- /dev/null +++ b/generated/symAction_range_eq_centralizer_glAction/lakefile.toml @@ -0,0 +1,27 @@ +name = "symAction_range_eq_centralizer_glAction" +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" diff --git a/generated/symAction_range_eq_centralizer_glAction/lean-toolchain b/generated/symAction_range_eq_centralizer_glAction/lean-toolchain new file mode 100644 index 000000000..e7e267fe4 --- /dev/null +++ b/generated/symAction_range_eq_centralizer_glAction/lean-toolchain @@ -0,0 +1,2 @@ +leanprover/lean4:v4.30.0-rc1 + diff --git a/generated/two_plus_two/lakefile.toml b/generated/two_plus_two/lakefile.toml index 8681843eb..6c95d87ac 100644 --- a/generated/two_plus_two/lakefile.toml +++ b/generated/two_plus_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" diff --git a/scripts/check_eval_workflow.py b/scripts/check_eval_workflow.py index f377dc369..88c524595 100644 --- a/scripts/check_eval_workflow.py +++ b/scripts/check_eval_workflow.py @@ -97,7 +97,12 @@ def main() -> int: try: ensure_repo_clean() problems = load_problems() - with tempfile.TemporaryDirectory(prefix="lean-eval-workflow-") as tmpdir: + # Place the tempdir under REPO_ROOT so `run_eval.score_problems` can + # compute `workspace_path.relative_to(gp.REPO_ROOT)` without ValueError + # (same workaround as `evaluate_submission.py`). + with tempfile.TemporaryDirectory( + prefix="lean-eval-workflow-", dir=gp.REPO_ROOT + ) as tmpdir: workspaces_root = pathlib.Path(tmpdir) / "workspaces" initial_summary = summarize_with_temp_workspaces(problems, workspaces_root) diff --git a/scripts/generate_projects.py b/scripts/generate_projects.py index 6002c4256..167a2c8ef 100644 --- a/scripts/generate_projects.py +++ b/scripts/generate_projects.py @@ -389,12 +389,25 @@ def extract_statement_text(problem: ProblemSpec, extracted: ExtractedTheorem) -> end = offset_for_line_column(source_text, end_line, end_column) declaration_text = source_text[start:end] theorem_name = local_theorem_name(extracted) - match = _theorem_by_pattern(theorem_name).search(declaration_text) - if not match: + # Find the theorem header to locate the start of the body. + header = re.search( + rf"(?:^|\s)theorem\s+{re.escape(theorem_name)}\b", + declaration_text, + re.DOTALL, + ) + if not header: + raise GenerationError( + f"Could not recover theorem statement text for '{problem.id}' from {source_path}" + ) + # Use rfind to locate the *last* `:= by` in the declaration text. + # This handles theorems whose type contains nested `haveI ... := by` + # clauses: the outer proof marker is always the last one. + last_by = declaration_text.rfind(":= by") + if last_by == -1: raise GenerationError( f"Could not recover theorem statement text for '{problem.id}' from {source_path}" ) - return match.group("body").strip() + return declaration_text[header.end():last_by].strip() def extract_source_text_for_range(source_text: str, source_range: tuple[int, int, int, int]) -> str: @@ -512,12 +525,13 @@ def render_challenge_deps(problem: ProblemSpec, extracted: ExtractedTheorem) -> return "import Mathlib\n\n" + challenge_deps_body -def extract_context_opens(problem: ProblemSpec) -> str: +def extract_context_opens(problem: ProblemSpec, *, include_namespaces: bool = False) -> str: source_path = module_source_path(problem.module) if not source_path.is_file(): raise GenerationError(f"Source file for module '{problem.module}' not found: {source_path}") lines = source_path.read_text(encoding="utf-8").splitlines() context_lines: list[str] = [] + namespace_stack: list[str] = [] in_body = False for line in lines: stripped = line.strip() @@ -530,8 +544,15 @@ def extract_context_opens(problem: ProblemSpec) -> str: stripped, ): break - if stripped.startswith("open "): + if stripped.startswith("namespace "): + namespace_stack.append(stripped.split(maxsplit=1)[1].strip()) + elif re.match(r"^end\b", stripped): + if namespace_stack: + namespace_stack.pop() + elif stripped.startswith("open "): context_lines.append(line) + if include_namespaces and namespace_stack: + context_lines.insert(0, "open " + ".".join(namespace_stack)) return "\n".join(context_lines) + ("\n\n" if context_lines else "") @@ -620,7 +641,9 @@ def render_workspace( if challenge_deps is not None else "import Mathlib\nimport Submission.Helpers\n\n" ) - context_open_block = extract_context_opens(problem) + context_open_block = extract_context_opens( + problem, include_namespaces=challenge_deps is not None + ) if context_open_block and not context_open_block.endswith("\n\n"): context_open_block += "\n" readme_lines = [