OpenAI Math is a mathematical theorem proving dataset released by FineEnvs in 2026, which organizes OpenAI's mathematical results into Lean formalized theorem proving environments, aiming to provide agents with strictly verifiable formal mathematical theorem proving tasks.

The dataset contains 369 Harbor task environments that have passed end-to-end validation, derived from 405 results formalized as Lean theorem statements in the OpenAI openai/math project, covering 214 result families and 17 mathematical fields.

The dataset employs an experimental validation filtering mechanism, including only tasks where OpenAI's original proofs can pass validation in the corresponding environments. Agents are required to complete the full proof of the original theorem by filling in proof placeholders marked with sorry within pre-configured sandbox environments equipped with Lean 4 and Mathlib.

Upon task completion, the validator checks the proof results in an isolated sandbox: it requires that the theorem statement exactly matches the original version, contains no incomplete sorry, uses only Lean standard axioms, and passes Lean kernel verification. A reward of 1 is granted if validation passes, otherwise a reward of 0 is granted.

Each task is configured by default with 4 CPU cores, 8 GB of memory, and 10 GB of disk space, with an execution time limit of 4 hours.

Dataset Composition

• tasks directory: Each validated problem corresponds to one Harbor task, containing the task description, Lean theorem statement, sandbox image recipe, validator, and reference solver.
• registry.json: Harbor registry entry [email protected].
• manifest.parquet: One row per task, with fields including field, result family, theorem name, reference proof size, and oracle result.
• generator directory: Code required to build sandbox images and regenerate tasks from openai/math.
• LICENSE, NOTICE, and LICENSE-openai-math: Licensing and attribution notices.