We use cookies for essential functionality and analytics. You can accept or reject analytics cookies.Cookie policy
OProofs Formal Lean 4 theorem-proof pairs produced as part of the OProver project. Fields Field Type Description formal_statement string Lean 4 theorem statement formal_proof string Lean 4 proof body cot_proof string | null Chain-of-thought reasoning preceding the proof, if available prompt string | null Generation prompt, if available Stats Records: 6,804,694 Files: 73 parquet shards (zstd compressed) Loading… See the full description on the dataset page: https://huggingface.co/datasets/m-a-p/OProofs.
Formal Lean 4 theorem-proof pairs produced as part of the OProver project.
| Field | Type | Description |
|---|---|---|
formal_statement | string | Lean 4 theorem statement |
formal_proof | string | Lean 4 proof body |
cot_proof | string | null | Chain-of-thought reasoning preceding the proof, if available |
prompt | string | null | Generation prompt, if available |
from datasets import load_dataset
ds = load_dataset("m-a-p/OProofs", split="train")
Mirrored from an external registry.
Last synced 7/28/2026
Preview not yet available for this dataset