raising-heart/openai-math
openai/math as Harbor environments: Harbor dataset on Hugging Face with 369 tasks. Experimental. Built on a research release that is itself new and not yet independently reviewed. Expect rough edges, and read any proof that scores 1 before relying on it.
Tasks
- Prove AbhyankarSathaye (openai/math family 049: A stable-coordinate counterexample in four variables) in Lean 4 with Mathlib; graded by…
- Prove AffineBernstein (openai/math family 353: The sharp dimension threshold for affine Bernstein rigidity) in Lean 4 with Mathlib; graded…
- Prove AlgorithmicThinTrees (openai/math family 174: Deterministic construction of strong thin spanning trees) in Lean 4 with Mathlib…
- Prove AmplitudeDamping (openai/math family 276: The classical capacity of generalized amplitude damping) in Lean 4 with Mathlib; graded by…
- Prove ArtinCAT0 (openai/math family 254: Classifying spaces and geometric obstructions for Artin groups) in Lean 4 with Mathlib; graded by…
- Prove ArtinParabolicIntersections (openai/math family 254: Classifying spaces and geometric obstructions for Artin groups) in Lean 4 with…
- Prove AsymptoticallyMinimalLittlewood (openai/math family 076: Ultraflat real Littlewood polynomials) in Lean 4 with Mathlib; graded by…
- Prove AtomicGaussian (openai/math family 090: Universal optimality of the triangular lattice) in Lean 4 with Mathlib; graded by Comparator…
- Prove AuslanderReiten (openai/math family 199: Counterexamples to conjectures of Auslander–Reiten, Tachikawa, and Nakayama) in Lean 4 with…
- Prove BackwardIntertwiners (openai/math family 293: A counterexample to the hyperinvariant-subspace problem) in Lean 4 with Mathlib…
- Prove BalancedBoxRouting (openai/math family 376: Universal computation in forced Navier–Stokes flows) in Lean 4 with Mathlib; graded by…
- Prove BalancedRyser (openai/math family 162: Counterexamples to Ryser's covering and Gyarfas's tree-cover conjectures) in Lean 4 with…
- Prove BalancedThreeStack (openai/math family 376: Universal computation in forced Navier–Stokes flows) in Lean 4 with Mathlib; graded by…
- Prove BallPacking (openai/math family 343: Sharp symplectic ball-packing criteria in higher dimensions) in Lean 4 with Mathlib; graded by…
- Prove BallPackingNecessity (openai/math family 343: Sharp symplectic ball-packing criteria in higher dimensions) in Lean 4 with Mathlib…
- Prove BarnetteHamiltonian (openai/math family 180: Barnette's Hamiltonian-cycle conjecture) in Lean 4 with Mathlib; graded by Comparator…
- Prove BassTorsionFree (openai/math family 207: The $\ell^1$-Bass and complex Bass trace conjectures) in Lean 4 with Mathlib; graded by…
- Prove BassTrace (openai/math family 207: The $\ell^1$-Bass and complex Bass trace conjectures) in Lean 4 with Mathlib; graded by…
- Prove BenjaminiSchramm (openai/math family 214: The Benjamini–Schramm nonuniqueness conjecture) in Lean 4 with Mathlib; graded by…
- Prove BernoulliNonflatInSeven (openai/math family 367: The critical dimension for the one-phase Bernoulli problem) in Lean 4 with Mathlib…
- Prove BiholderTransport (openai/math family 360: Villani’s convexity conjecture and regular optimal transport) in Lean 4 with Mathlib…
- Prove BinPackingGap (openai/math family 118: Unbounded bin-packing gaps and the modified integer round-up conjecture) in Lean 4 with…
- Prove BinaryEditLower (openai/math family 099: The sharp distortion of edit distance into $\ell 1$) in Lean 4 with Mathlib; graded by…
- Prove BinaryMatching (openai/math family 113: Approximate counting and the perfect-matching entropy conjecture) in Lean 4 with Mathlib…
- Prove BinarySweep (openai/math family 238: Optimal logarithmic mixing of the Thorp shuffle) in Lean 4 with Mathlib; graded by Comparator…
- Prove BipartiteCrossing (openai/math family 165: Exact crossing numbers of complete and complete bipartite graphs) in Lean 4 with Mathlib…
- Prove BogomolovPopInjectivity (openai/math family 009: Bogomolov–Pop and Milnor $K$-theoretic reconstruction) in Lean 4 with Mathlib…
- Prove BoltzmannNonuniqueness (openai/math family 363: Boltzmann nonuniqueness with exact local conservation) in Lean 4 with Mathlib…
- Prove BooneHigman (openai/math family 250: The Boone–Higman conjecture and higher finiteness) in Lean 4 with Mathlib; graded by Comparator…
- Prove BorsukNine (openai/math family 156: Borsuk's conjecture fails in dimension nine) in Lean 4 with Mathlib; graded by Comparator in a…
- Prove BoundedRecovery (openai/math family 290: Connes' bicentralizer conjecture and relative bicentralizers) in Lean 4 with Mathlib…
- Prove BoundedTreePotentials (openai/math family 331: Asymptotic midpoint uniform convexity without asymptotically uniformly convex…
- Prove BoundedTreewidthL1 (openai/math family 089: Bounded-distortion $L 1$ embeddings of planar and bounded-treewidth graphs) in Lean 4…
- Prove Brenier (openai/math family 374: Sharp one-third stability of optimal transport maps) in Lean 4 with Mathlib; graded by Comparator…
- Prove Brennan (openai/math family 072: Brennan's conjecture and a counterexample to Kraetzer's prediction) in Lean 4 with Mathlib; graded…
- Prove BrennanSharp (openai/math family 072: Brennan's conjecture and a counterexample to Kraetzer's prediction) in Lean 4 with Mathlib…
- Prove BufferedIsing (openai/math family 218: Conformal universality for weakly interacting and disordered Ising models) in Lean 4 with…
- Prove C0Absorption (openai/math family 324: Lipschitz equivalence without linear isomorphism) in Lean 4 with Mathlib; graded by Comparator…
- Prove C1EntropyCounterexample (openai/math family 151: A $C^1$ counterexample to Shub’s entropy conjecture) in Lean 4 with Mathlib; graded…
- Prove CannonGeometricAction (openai/math family 246: Cannon's conjecture) in Lean 4 with Mathlib; graded by Comparator in a separate…
- Prove CayleyPercolation (openai/math family 214: The Benjamini–Schramm nonuniqueness conjecture) in Lean 4 with Mathlib; graded by…
- Prove CHObstruction (openai/math family 240: Shelah's eventual categoricity conjecture) in Lean 4 with Mathlib; graded by Comparator in a…
- Prove CharacterCriterion (openai/math family 299: The Kirchberg–R\o rdam character criterion) in Lean 4 with Mathlib; graded by Comparator…
- Prove ChoicelessPolynomialTime (openai/math family 243: Choiceless counting does not capture polynomial time) in Lean 4 with Mathlib…
- Prove CirculantHadamard (openai/math family 179: The circulant Hadamard conjecture) in Lean 4 with Mathlib; graded by Comparator in a…
- Prove CKSBondiPenrose (openai/math family 260: Spacetime Penrose inequalities and rigidity) in Lean 4 with Mathlib; graded by Comparator…
- Prove ClassicalON (openai/math family 215: Massive continuum limits and exact mass asymptotics for planar $O(n)$ models) in Lean 4 with…
- Prove CliqueFreeLog (openai/math family 184: Coloring and independence in graphs with forbidden subgraphs) in Lean 4 with Mathlib; graded…
- Prove CoboundaryExpanders (openai/math family 177: Bounded-degree coboundary expanders in every dimension) in Lean 4 with Mathlib; graded…
- Prove CommonBasesFPRAS (openai/math family 114: Approximate counting of common integer polymatroid bases) in Lean 4 with Mathlib; graded…
- Prove CommutingDerivations (openai/math family 049: A stable-coordinate counterexample in four variables) in Lean 4 with Mathlib; graded…
- Prove CompactBanach (openai/math family 098: A negative answer to the Lang–Plaut problem) in Lean 4 with Mathlib; graded by Comparator in…
- Prove CompleteCrossing (openai/math family 165: Exact crossing numbers of complete and complete bipartite graphs) in Lean 4 with Mathlib…
- Prove CompleteCrouzeix (openai/math family 325: The complete Crouzeix conjecture) in Lean 4 with Mathlib; graded by Comparator in a…
- Prove ComplexCancellation (openai/math family 047: Complex counterexamples to cancellation and affine fibrations) in Lean 4 with Mathlib…
- Prove Conductivity (openai/math family 365: Joint metric and connection recovery from one boundary patch) in Lean 4 with Mathlib; graded…
- Prove ConjugatePoints (openai/math family 358: A three-manifold with no conjugate points and no nonpositively curved metric) in Lean 4…
- Prove ContingencyTables (openai/math family 115: Sampling and counting contingency tables with arbitrary margins) in Lean 4 with Mathlib…
- Prove ContinuousCircleWeight (openai/math family 293: A counterexample to the hyperinvariant-subspace problem) in Lean 4 with Mathlib…
- Prove ContinuumTransition (openai/math family 228: Continuum phase transitions for radial pair potentials) in Lean 4 with Mathlib; graded…
- Prove CoordinateSweeps (openai/math family 238: Optimal logarithmic mixing of the Thorp shuffle) in Lean 4 with Mathlib; graded by…
- Prove CoordinateTrace (openai/math family 238: Optimal logarithmic mixing of the Thorp shuffle) in Lean 4 with Mathlib; graded by…
- Prove Cotype (openai/math family 326: The cotype–cotype conjecture under the approximation property) in Lean 4 with Mathlib; graded by…
- Prove CoulombCounterexample (openai/math family 373: Nonattainment in three-marginal Coulomb transport) in Lean 4 with Mathlib; graded by…
- Prove CoulombIonization (openai/math family 263: The ionization and generalized ionization conjectures) in Lean 4 with Mathlib; graded by…
- Prove CoulombRadii (openai/math family 263: The ionization and generalized ionization conjectures) in Lean 4 with Mathlib; graded by…
- Prove CourtadeKumar (openai/math family 119: The Courtade–Kumar and Hellinger conjectures) in Lean 4 with Mathlib; graded by Comparator in…
- Prove CoveringDensity (openai/math family 092: The optimal order of convex-body covering density) in Lean 4 with Mathlib; graded by…
- Prove CriticalPercolation (openai/math family 213: No infinite critical clusters on quasi-transitive graphs) in Lean 4 with Mathlib…
- Prove CriticalSK (openai/math family 227: The dynamical phase transition in the Sherrington–Kirkpatrick model) in Lean 4 with Mathlib…
- Prove CriticalSKMixing (openai/math family 227: The dynamical phase transition in the Sherrington–Kirkpatrick model) in Lean 4 with…
- Prove CriticalStripMass (openai/math family 237: The three-quarter diameter exponent for honeycomb walks) in Lean 4 with Mathlib; graded…
- Prove CriticalZ3 (openai/math family 213: No infinite critical clusters on quasi-transitive graphs) in Lean 4 with Mathlib; graded by…
- Prove CrouzeixHilbert (openai/math family 325: The complete Crouzeix conjecture) in Lean 4 with Mathlib; graded by Comparator in a…
- Prove CubicTorus (openai/math family 354: Isoperimetric regions in the cubic three-torus) in Lean 4 with Mathlib; graded by Comparator in…
- Prove CycleDecomposition (openai/math family 181: The Erd\H{o}s–Gallai cycle-decomposition conjecture) in Lean 4 with Mathlib; graded by…
- Prove CylinderCovering (openai/math family 100: A counterexample to Bang's cylinder-covering bound) in Lean 4 with Mathlib; graded by…
- Prove DaugavetModuli (openai/math family 331: Asymptotic midpoint uniform convexity without asymptotically uniformly convex renorming) in…
- Prove DegreeRigidity (openai/math family 241: Rigidity of the Turing degrees) in Lean 4 with Mathlib; graded by Comparator in a separate…
- Prove DeligneDrinfeld (openai/math family 008: The Deligne–Drinfeld conjecture) in Lean 4 with Mathlib; graded by Comparator in a separate…
- Prove DepthFive (openai/math family 135: Sharp homogeneous depth-five complexity of matrix products) in Lean 4 with Mathlib; graded by…
- Prove DepthThree (openai/math family 112: Beyond the square-root exponent for depth-three circuits) in Lean 4 with Mathlib; graded by…
- Prove DiamondDistortion (openai/math family 331: Asymptotic midpoint uniform convexity without asymptotically uniformly convex renorming)…
- Prove DilutedSpin (openai/math family 221: The Mezard–Parisi formula for diluted spin glasses) in Lean 4 with Mathlib; graded by…
- Prove DimensionTenChannel (openai/math family 272: Entanglement without secret key and the PPT-square conjecture) in Lean 4 with Mathlib…
- Prove DimensionTenPair (openai/math family 272: Entanglement without secret key and the PPT-square conjecture) in Lean 4 with Mathlib…
- Prove DirectCrouzeix (openai/math family 325: The complete Crouzeix conjecture) in Lean 4 with Mathlib; graded by Comparator in a separate…
- Prove DirectedFeedback (openai/math family 102: The Unique Games Conjecture and optimal approximation thresholds) in Lean 4 with Mathlib…
- Prove DirectionalBallisticity (openai/math family 220: Directional zero–one laws and ballisticity in random environments) in Lean 4 with…
- Prove DirectionalWalk (openai/math family 220: Directional zero–one laws and ballisticity in random environments) in Lean 4 with Mathlib…
- Prove DiscreteLipschitzFree (openai/math family 330: A negative answer to Kalton's Lipschitz-free approximation question) in Lean 4 with…
- Prove DiskMaximal (openai/math family 085: Endpoint regularity of the planar centered maximal function) in Lean 4 with Mathlib; graded by…
- Prove Dixmier (openai/math family 251: Amenability, unitarizability, and Ulam stability) in Lean 4 with Mathlib; graded by Comparator in a…
- Prove DixmierAllDiscrete (openai/math family 251: Amenability, unitarizability, and Ulam stability) in Lean 4 with Mathlib; graded by…
- Prove DoublingHilbert (openai/math family 098: A negative answer to the Lang–Plaut problem) in Lean 4 with Mathlib; graded by Comparator…
- Prove DuttaDomain (openai/math family 194: Lech's multiplicity conjecture) in Lean 4 with Mathlib; graded by Comparator in a separate…
- Prove DyadicAvoidance (openai/math family 084: The geometric case of the Erd\H{o}s similarity conjecture) in Lean 4 with Mathlib; graded…
- Prove EditApproximation (openai/math family 121: Almost-linear expected-time approximation of edit distance) in Lean 4 with Mathlib…
- Prove EditDistance (openai/math family 099: The sharp distortion of edit distance into $\ell 1$) in Lean 4 with Mathlib; graded by…
- Prove EgyptianFractions (openai/math family 025: Erd\H{o}s’s short Egyptian-fraction conjecture) in Lean 4 with Mathlib; graded by…
- Prove EilenbergGanea (openai/math family 249: A finitely generated counterexample to Eilenberg–Ganea) in Lean 4 with Mathlib; graded by…
- Prove ElasticityUniqueness (openai/math family 372: Global uniqueness in smooth isotropic elasticity) in Lean 4 with Mathlib; graded by…
- Prove ElementaryPositivity (openai/math family 169: The Shareshian–Wachs $e$-positivity conjecture) in Lean 4 with Mathlib; graded by…
- Prove EntangledGames (openai/math family 277: Threshold repetition for entangled games) in Lean 4 with Mathlib; graded by Comparator in a…
- Prove EntropyPhotonNumber (openai/math family 273: The entropy photon-number inequality) in Lean 4 with Mathlib; graded by Comparator in a…
- Prove EuclideanFiveColor (openai/math family 158: The Euclidean plane cannot be colored with five colors) in Lean 4 with Mathlib; graded…
- Prove EuclideanRamsey (openai/math family 172: Classification of finite Euclidean Ramsey configurations) in Lean 4 with Mathlib; graded by…
- Prove EuclideanRamseyCircle (openai/math family 172: Classification of finite Euclidean Ramsey configurations) in Lean 4 with Mathlib…
- Prove EuclideanRamseyNine (openai/math family 172: Classification of finite Euclidean Ramsey configurations) in Lean 4 with Mathlib…
- Prove EuclideanRamseyQuadratic (openai/math family 172: Classification of finite Euclidean Ramsey configurations) in Lean 4 with Mathlib…
- Prove EuclideanRamseySpherical (openai/math family 172: Classification of finite Euclidean Ramsey configurations) in Lean 4 with Mathlib…
- Prove EuclideanRamseyTransitive (openai/math family 172: Classification of finite Euclidean Ramsey configurations) in Lean 4 with Mathlib…
- Prove EvenBarker (openai/math family 179: The circulant Hadamard conjecture) in Lean 4 with Mathlib; graded by Comparator in a separate…
- Prove ExactFourier (openai/math family 130: Fourier transforms below $n\log n$) in Lean 4 with Mathlib; graded by Comparator in a separate…
- Prove ExactInfiniteness (openai/math family 303: From ordinary to strong pure infiniteness) in Lean 4 with Mathlib; graded by Comparator…
- Prove ExactQuantumFactoring (openai/math family 279: Exact quantum factoring over a fixed finite gate set) in Lean 4 with Mathlib; graded…
- Prove FactorGeneration (openai/math family 296: The generator problem for finite factors) in Lean 4 with Mathlib; graded by Comparator in…
- Prove FalconerAllDimensions (openai/math family 073: The Falconer distance conjecture) in Lean 4 with Mathlib; graded by Comparator in a…
- Prove FillingCoefficient (openai/math family 337: Cartan–Hadamard isoperimetry and CAT$(0)$ fillings) in Lean 4 with Mathlib; graded by…
- Prove FiniteCircle (openai/math family 099: The sharp distortion of edit distance into $\ell 1$) in Lean 4 with Mathlib; graded by…
- Prove FiniteCongruenceGraph (openai/math family 206: Finite lattice representation: counterexamples and undecidability) in Lean 4 with…
- Prove FiniteEntropySeparation (openai/math family 298: A counterexample to Voiculescu’s free-entropy equality conjecture) in Lean 4 with…
- Prove FiniteFactor (openai/math family 293: A counterexample to the hyperinvariant-subspace problem) in Lean 4 with Mathlib; graded by…
- Prove FinitisticAsymmetry (openai/math family 198: A counterexample to the little finitistic-dimension conjecture) in Lean 4 with Mathlib…
- Prove FixedClauseThreshold (openai/math family 235: Random-SAT thresholds, sharp variance and computability) in Lean 4 with Mathlib…
- Prove FKCRT (openai/math family 211: Geometry, diffusion, and spectra of random planar maps) in Lean 4 with Mathlib; graded by Comparator…
- Prove ForcedNavierStokesComputation (openai/math family 376: Universal computation in forced Navier–Stokes flows) in Lean 4 with Mathlib…
- Prove ForestSpace (openai/math family 331: Asymptotic midpoint uniform convexity without asymptotically uniformly convex renorming) in…
- Prove FormulaHitting (openai/math family 116: Uniform identity testing for noncommutative formulas) in Lean 4 with Mathlib; graded by…
- Prove FoulkesHowe (openai/math family 210: Foulkes’ conjecture for sixth powers and quadratic stabilization) in Lean 4 with Mathlib…
- Prove FourRowPermanent (openai/math family 238: Optimal logarithmic mixing of the Thorp shuffle) in Lean 4 with Mathlib; graded by…
- Prove FreeIsing (openai/math family 236: The factor-of-IID threshold for free Ising states on trees) in Lean 4 with Mathlib; graded by…
- Prove FreeUniformSpanningForest (openai/math family 231: The free uniform spanning forest is a factor of IID) in Lean 4 with Mathlib…
- Prove GammaPassage (openai/math family 212: No bigeodesics and smooth limit shapes in planar first-passage percolation) in Lean 4 with…
- Prove GaussianFiniteEntropy (openai/math family 140: Memory–sample lower bounds for noiseless Gaussian regression) in Lean 4 with Mathlib…
- Prove GaussianInformation (openai/math family 140: Memory–sample lower bounds for noiseless Gaussian regression) in Lean 4 with Mathlib…
- Prove GaussianMoat (openai/math family 028: The Gaussian moat conjecture) in Lean 4 with Mathlib; graded by Comparator in a separate…
- Prove GaussianPropeller (openai/math family 096: The Gaussian propeller conjecture) in Lean 4 with Mathlib; graded by Comparator in a…
- Prove GaussianReplacement (openai/math family 140: Memory–sample lower bounds for noiseless Gaussian regression) in Lean 4 with Mathlib…
- Prove GeneralMahler (openai/math family 087: The Mahler conjectures and symplectic width) in Lean 4 with Mathlib; graded by Comparator in…
- Prove GeneralizedStarHeight (openai/math family 134: Generalized star height at most three) in Lean 4 with Mathlib; graded by Comparator…
- Prove GotsmanLinial (openai/math family 127: The asymptotic Gotsman–Linial conjecture) in Lean 4 with Mathlib; graded by Comparator in a…
- Prove GrahamSpherical (openai/math family 172: Classification of finite Euclidean Ramsey configurations) in Lean 4 with Mathlib; graded by…
- Prove GrothendieckElementaryExpansion (openai/math family 312: The Grothendieck homotopy hypothesis) in Lean 4 with Mathlib; graded by…
- Prove GroupRingDeterminant (openai/math family 197: Nonsofic groups and group-ring counterexamples) in Lean 4 with Mathlib; graded by…
- Prove HadamardCubeFiber (openai/math family 266: Exactly three mutually unbiased bases in dimension six) in Lean 4 with Mathlib; graded by…
- Prove HalvingLines (openai/math family 183: Power savings for planar halving lines and $k$-sets) in Lean 4 with Mathlib; graded by…
- Prove HardSphere (openai/math family 267: Positive-temperature Bose–Einstein condensation and quantum depletion) in Lean 4 with Mathlib…
- Prove HarmonicArtin (openai/math family 254: Classifying spaces and geometric obstructions for Artin groups) in Lean 4 with Mathlib…
- Prove HarmonicGrowth (openai/math family 361: Counterexamples to Yau's harmonic dimension bound) in Lean 4 with Mathlib; graded by…
219 more tasks.