OpenAI Math は、FineEnvs により 2026 年にリリースされた、OpenAI の数学的な結果を Lean 形式の定理証明環境に整理した数学定理証明データセットであり、エージェントに対して厳密に検証可能な形式化された数学定理証明タスクを提供することを目的としています。

このデータセットには、OpenAI の openai/math プロジェクトにおいて Lean の定理ステートメントとして形式化された 405 件の結果に由来する、エンドツーエンドの検証を通過した 369 個の Harbor タスク環境が含まれており、214 の結果ファミリーと 17 の数学分野をカバーしています。

データセットは実験的な検証フィルター機構を採用しており、OpenAI の元の証明が対応する環境で検証を通過したタスクのみを収録しています。エージェントは、事前に設定された Lean 4 および Mathlib のサンドボックス環境内で、sorry でマークされた証明プレースホルダーを補完し、元の定理の完全な証明を完了する必要があります。

タスク完了後、バリデータは独立したサンドボックス内で証明結果を確認します。定理ステートメントが元のバージョンと完全に一致していること、未完了の sorry が存在しないこと、Lean の標準公理のみを使用していること、そして証明が Lean コアによって検証されることなどが必要です。検証に合格した場合は報酬 1 を、それ以外の場合は報酬 0 を獲得します。

各タスクのデフォルト構成は、CPU 4 コア、メモリ 8 GB、ディスク容量 10 GB で、実行制限時間は 4 時間です。

データセットの構成

• tasks ディレクトリ：検証を通過した各問題に対応する Harbor タスクが含まれており、タスクの説明、Lean の定理ステートメント、サンドボックスイメージのレシピ、バリデータ、およびリファレンスソルバーが含まれています。
• registry.json：Harbor レジストリエントリー [email protected]。
• manifest.parquet：各タスクにつき 1 行で、分野、結果ファミリー、定理名、リファレンス証明の規模、oracle result などのフィールドが含まれています。
• generator ディレクトリ：サンドボックスイメージの構築および openai/math からのタスク再生成に必要なコードが含まれています。
• LICENSE、NOTICE、LICENSE-openai-math：ライセンスおよび帰属に関する説明。