banach1729/goedel-workbook-lean427
Goedel Workbook Proofs — Lean 4.27 29,750 competition-math proofs from Goedel-LM/Lean-workbook-proofs, migrated from Lean 4.8 to Lean 4.27.0 / Mathlib v4.27.0. The original proofs were generated by DeepSeek-Prover-V1.5 against the Lean Workbook problem set. Quick Stats Metric Value Total proofs 29,750 Compiling on Lean 4.27 28,016 (94.1%) Traced tactic pairs 60,341 Theorems with traced pairs 24,879 Unique tactic heads 73 Median proof depth 1… See the full description on the dataset page: https://huggingface.co/datasets/banach1729/goedel-workbook-lean427.
| Author / organization | banach1729 |
|---|---|
| License (as declared) | apache-2.0 |
| Downloads | 1.4K (as reported by Hugging Face) |
| Likes | 0 |
| Created | 22 March 2026 |
| Last updated at source | 22 March 2026 |
Popularity, last 3 days
1,357 now (+42 since 2026-10-16). Counts as reported by the source, snapshotted daily by Silytics.
Silytics shows public metadata from Hugging Face and links to the original. Information may be incomplete or out of date. Last refreshed 18 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.