hmzprover/proofs-public
Lean 4 Proofs (public sources) 1,560,974 Lean 4 theorems and definitions from public Lean libraries and datasets. Each row is one declaration: column content nl_statement the statement in natural language nl_proof a natural-language proof; null when there is none (42,408 rows have one) lean_statement the Lean 4 declaration header, e.g. theorem foo (x : ℕ) : x ≤ x + 1 lean_proof the Lean 4 proof (or definition body) that follows the header, e.g. := by omega… See the full description on the dataset page: https://huggingface.co/datasets/hmzprover/proofs-public.
| Author / organization | hmzprover |
|---|---|
| License (as declared) | cc-by-sa-4.0 |
| Downloads | 0 (as reported by Hugging Face) |
| Likes | 0 |
| Created | 23 October 2026 |
| Last updated at source | 23 October 2026 |
Silytics shows public metadata from Hugging Face and links to the original. Information may be incomplete or out of date. Last refreshed 23 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.