bkhtmm/openai-math-lemmas
openai-math-lemmas: Harbor dataset on Hugging Face with 47 tasks. From one formal-math problem to 47 independently checkable Lean proof tasks. We extracted 47 supporting lemmas from the reference proof of honeycomb-free-energy in FineEnvs/openai-math and packaged them as self-contained proof…
Tasks
- Prove OAI.HoneycombForce.displacement shift using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.displacement split using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.endpoint drop using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.endpoint one type using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.endpoint rayPath using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.endpoint take using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.exists logPartition limit using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.maxPartition log div bddBelow using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.maxPartition log linear lower using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.maxPartition log subadditive using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.maxPartition pos using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.maxPartition submultiplicative using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.maxPartition succ le using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.maxPartition zero using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.mem neighbors iff using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.mem saws iff using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.mem saws shift using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.mem walkLists iff using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.partition eq base using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.partition le maxPartition using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.partition le mul maxPartition using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.partition nonneg using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.partition pos using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.partition shift using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.partition split using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.partition succ opposite using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.partition zero using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.position rowVertex using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.position shift using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.ray adj using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.ray injective using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.ray zero using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.rayPath mem using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.rho nonneg using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.rho pos using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.rowPath projection lower using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.rowVertex adj using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.rowVertex injective using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.saws nonempty using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.saws shift using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.saws zero using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.shiftVertex adj using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.shiftVertex injective using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.shiftVertex shift using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.shiftVertex zero using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.splitWalk injective using the supplied Honeycomb Free Energy source prefix.
- Prove OAI.HoneycombForce.splitWalk mem using the supplied Honeycomb Free Energy source prefix.