OProofs

# 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 ```python from datasets import load_dataset ds = load_dataset("m-a-p/OProofs", split="train") ```