OProver/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… See the full description on the dataset page: https://huggingface.co/datasets/OProver/OProofs.
| Author / organization | OProver |
|---|---|
| License (as declared) | apache-2.0 |
| Downloads | 621 (as reported by Hugging Face) |
| Likes | 0 |
| Created | 18 May 2026 |
| Last updated at source | 18 May 2026 |
Recent changes
- 16 Oct 2026 Description: 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 → 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
Changes detected by Silytics between refreshes of the source.
Silytics shows public metadata from Hugging Face and links to the original. Information may be incomplete or out of date. Last refreshed 16 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.