First 17 rows of test
| namestring | instructionstring | descriptionstring | keywordsList | schema_versionstring | configJson | metadataJson | filesList | locationstring |
|---|---|---|---|---|---|---|---|---|
| openai-math/abhyankar-sathaye | # openai/math challenge `AbhyankarSathaye` (family 049) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 049 of the release, *A stable-coordi… | Prove AbhyankarSathaye (openai/math family 049: A stable-coordinate counterexample in four variables) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","algebraic-and-complex-geometry"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/abhyankar-sathaye","version":"1.0.0","description":"Prove AbhyankarSathaye (openai/math family 049: A stable-coordinate counterexample in four variables) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox.","keyw… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/AbhyankarSathaye.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at the … | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/abhyankar-sathaye |
| openai-math/affine-bernstein | # openai/math challenge `AffineBernstein` (family 353) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 353 of the release, *The sharp dimens… | Prove AffineBernstein (openai/math family 353: The sharp dimension threshold for affine Bernstein rigidity) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. |
| ["lean4","mathlib","theorem-proving","openai-math","differential-geometry"] |
| 1.4 |
| {"schema_version":"1.4","task":{"name":"openai-math/affine-bernstein","version":"1.0.0","description":"Prove AffineBernstein (openai/math family 353: The sharp dimension threshold for affine Bernstein rigidity) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox.",… |
| {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/AffineBernstein.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at the d… |
| ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… |
| tasks/affine-bernstein |
| openai-math/algorithmic-thin-trees | # openai/math challenge `AlgorithmicThinTrees` (family 174) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 174 of the release, *Determinist… | Prove AlgorithmicThinTrees (openai/math family 174: Deterministic construction of strong thin spanning trees) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","combinatorics"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/algorithmic-thin-trees","version":"1.0.0","description":"Prove AlgorithmicThinTrees (openai/math family 174: Deterministic construction of strong thin spanning trees) in Lean 4 with Mathlib; graded by Comparator in a separate sa… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/AlgorithmicThinTrees.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at … | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/algorithmic-thin-trees |
| openai-math/amplitude-damping | # openai/math challenge `AmplitudeDamping` (family 276) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 276 of the release, *The classical c… | Prove AmplitudeDamping (openai/math family 276: The classical capacity of generalized amplitude damping) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","mathematical-physics"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/amplitude-damping","version":"1.0.0","description":"Prove AmplitudeDamping (openai/math family 276: The classical capacity of generalized amplitude damping) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox.","k… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/AmplitudeDamping.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at the … | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/amplitude-damping |
| openai-math/artin-cat0 | # openai/math challenge `ArtinCAT0` (family 254) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 254 of the release, *Classifying spaces and… | Prove ArtinCAT0 (openai/math family 254: Classifying spaces and geometric obstructions for Artin groups) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","group-theory"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/artin-cat0","version":"1.0.0","description":"Prove ArtinCAT0 (openai/math family 254: Classifying spaces and geometric obstructions for Artin groups) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox.","keywords… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/ArtinCAT0.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at the dataset… | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/artin-cat0 |
| openai-math/artin-parabolic-intersections | # openai/math challenge `ArtinParabolicIntersections` (family 254) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 254 of the release, *Clas… | Prove ArtinParabolicIntersections (openai/math family 254: Classifying spaces and geometric obstructions for Artin groups) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","group-theory"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/artin-parabolic-intersections","version":"1.0.0","description":"Prove ArtinParabolicIntersections (openai/math family 254: Classifying spaces and geometric obstructions for Artin groups) in Lean 4 with Mathlib; graded by Compara… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/ArtinParabolicIntersections.lean from openai/math, (c) OpenAI, unchanged; see NOT… | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/artin-parabolic-intersections |
| openai-math/asymptotically-minimal-littlewood | # openai/math challenge `AsymptoticallyMinimalLittlewood` (family 076) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 076 of the release, *… | Prove AsymptoticallyMinimalLittlewood (openai/math family 076: Ultraflat real Littlewood polynomials) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","real-and-complex-analysis"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/asymptotically-minimal-littlewood","version":"1.0.0","description":"Prove AsymptoticallyMinimalLittlewood (openai/math family 076: Ultraflat real Littlewood polynomials) in Lean 4 with Mathlib; graded by Comparator in a separate… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/AsymptoticallyMinimalLittlewood.lean from openai/math, (c) OpenAI, unchanged; see… | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/asymptotically-minimal-littlewood |
| openai-math/atomic-gaussian | # openai/math challenge `AtomicGaussian` (family 090) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 090 of the release, *Universal optimal… | Prove AtomicGaussian (openai/math family 090: Universal optimality of the triangular lattice) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","convex-and-metric-geometry"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/atomic-gaussian","version":"1.0.0","description":"Prove AtomicGaussian (openai/math family 090: Universal optimality of the triangular lattice) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox.","keywords":["le… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/AtomicGaussian.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at the da… | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/atomic-gaussian |
| openai-math/auslander-reiten | # openai/math challenge `AuslanderReiten` (family 199) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 199 of the release, *Counterexamples … | Prove AuslanderReiten (openai/math family 199: Counterexamples to conjectures of Auslander–Reiten, Tachikawa, and Nakayama) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","algebra"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/auslander-reiten","version":"1.0.0","description":"Prove AuslanderReiten (openai/math family 199: Counterexamples to conjectures of Auslander–Reiten, Tachikawa, and Nakayama) in Lean 4 with Mathlib; graded by Comparator in a sep… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/AuslanderReiten.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at the d… | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/auslander-reiten |
| openai-math/backward-intertwiners | # openai/math challenge `BackwardIntertwiners` (family 293) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 293 of the release, *A counterex… | Prove BackwardIntertwiners (openai/math family 293: A counterexample to the hyperinvariant-subspace problem) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","operator-algebras"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/backward-intertwiners","version":"1.0.0","description":"Prove BackwardIntertwiners (openai/math family 293: A counterexample to the hyperinvariant-subspace problem) in Lean 4 with Mathlib; graded by Comparator in a separate sand… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/BackwardIntertwiners.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at … | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/backward-intertwiners |
| openai-math/balanced-box-routing | # openai/math challenge `BalancedBoxRouting` (family 376) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 376 of the release, *Universal com… | Prove BalancedBoxRouting (openai/math family 376: Universal computation in forced Navier–Stokes flows) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","partial-differential-equations"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/balanced-box-routing","version":"1.0.0","description":"Prove BalancedBoxRouting (openai/math family 376: Universal computation in forced Navier–Stokes flows) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox.","… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/BalancedBoxRouting.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at th… | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/balanced-box-routing |
| openai-math/balanced-ryser | # openai/math challenge `BalancedRyser` (family 162) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 162 of the release, *Counterexamples to… | Prove BalancedRyser (openai/math family 162: Counterexamples to Ryser's covering and Gyarfas's tree-cover conjectures) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","combinatorics"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/balanced-ryser","version":"1.0.0","description":"Prove BalancedRyser (openai/math family 162: Counterexamples to Ryser's covering and Gyarfas's tree-cover conjectures) in Lean 4 with Mathlib; graded by Comparator in a separate s… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/BalancedRyser.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at the dat… | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/balanced-ryser |
| openai-math/balanced-three-stack | # openai/math challenge `BalancedThreeStack` (family 376) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 376 of the release, *Universal com… | Prove BalancedThreeStack (openai/math family 376: Universal computation in forced Navier–Stokes flows) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","partial-differential-equations"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/balanced-three-stack","version":"1.0.0","description":"Prove BalancedThreeStack (openai/math family 376: Universal computation in forced Navier–Stokes flows) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox.","… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/BalancedThreeStack.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at th… | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/balanced-three-stack |
| openai-math/ball-packing-necessity | # openai/math challenge `BallPackingNecessity` (family 343) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 343 of the release, *Sharp sympl… | Prove BallPackingNecessity (openai/math family 343: Sharp symplectic ball-packing criteria in higher dimensions) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","differential-geometry"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/ball-packing-necessity","version":"1.0.0","description":"Prove BallPackingNecessity (openai/math family 343: Sharp symplectic ball-packing criteria in higher dimensions) in Lean 4 with Mathlib; graded by Comparator in a separate… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/BallPackingNecessity.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at … | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/ball-packing-necessity |
| openai-math/ball-packing | # openai/math challenge `BallPacking` (family 343) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 343 of the release, *Sharp symplectic bal… | Prove BallPacking (openai/math family 343: Sharp symplectic ball-packing criteria in higher dimensions) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","differential-geometry"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/ball-packing","version":"1.0.0","description":"Prove BallPacking (openai/math family 343: Sharp symplectic ball-packing criteria in higher dimensions) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox.","keyword… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/BallPacking.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at the datas… | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/ball-packing |
| openai-math/barnette-hamiltonian | # openai/math challenge `BarnetteHamiltonian` (family 180) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 180 of the release, *Barnette's H… | Prove BarnetteHamiltonian (openai/math family 180: Barnette's Hamiltonian-cycle conjecture) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","combinatorics"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/barnette-hamiltonian","version":"1.0.0","description":"Prove BarnetteHamiltonian (openai/math family 180: Barnette's Hamiltonian-cycle conjecture) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox.","keywords":[… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/BarnetteHamiltonian.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at t… | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/barnette-hamiltonian |
| openai-math/bass-torsion-free | # openai/math challenge `BassTorsionFree` (family 207) Prove the following result from OpenAI's [openai/math](https://github.com/openai/math) release in Lean 4, with a proof the Lean kernel accepts. Context: this statement belongs to family 207 of the release, *The $\ell^1$-Bas… | Prove BassTorsionFree (openai/math family 207: The $\ell^1$-Bass and complex Bass trace conjectures) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox. | ["lean4","mathlib","theorem-proving","openai-math","algebra"] | 1.4 | {"schema_version":"1.4","task":{"name":"openai-math/bass-torsion-free","version":"1.0.0","description":"Prove BassTorsionFree (openai/math family 207: The $\\ell^1$-Bass and complex Bass trace conjectures) in Lean 4 with Mathlib; graded by Comparator in a separate sandbox.","keyw… | {"source":"https://github.com/openai/math","source_commit":"adc7f1241b42e322a6451854ab7e4b4c146bf78a","source_license":"Apache-2.0","source_notice":"tests/Challenge.lean is lean/ComparatorChallenges/BassTorsionFree.lean from openai/math, (c) OpenAI, unchanged; see NOTICE at the d… | ["environment/Dockerfile","environment/fetch_mathlib.sh","environment/lake-manifest.json","environment/lakefile.lean","environment/lean_setup.sh","environment/pack_submission.py","instruction.md","solution/closure.txt","solution/reference.py","solution/solve.sh","task.toml","test… | tasks/bass-torsion-free |
