m-a-p/

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

Records: 6,804,694 Files: 73 parquet shards (zstd compressed)

from… See the full description on the dataset page: https://huggingface.co/datasets/m-a-p/OProofs.