lean4
leandojo-lean4-retriever-byt5-smallleandojo-lean4-tacgen-byt5-smallleandojo-lean4-retriever-tacgen-byt5-smallct2-leandojo-lean4-tacgen-byt5-smallct2-leandojo-lean4-retriever-byt5-smallleandojo-lean4-retriever-byt5-small-hammerleandojo-lean4-tacgen-byt5-small-randomleandojo-lean4-tacgen-byt5-small-novel-premises
Datasets
All datasets matching “lean4”minif2f-lean4Fixing the errors in some formal statements and informal proofs of minif2f-lean4.
Lean4-EquationalTheories
Lean4-EquationalTheories
Structured dataset from equational_theories — Terence Tao's magma equations project.
Source
Repository: https://github.com/teorth/equational_theories
Commit: 3f3999d958c5e289c7f5a063479af9dac122a7a8
Files: 1301
License: apache-2.0
Schema
Column
Type
Description
statement
string
Declaration signature/claim with the leading keyword removed (verbatim slice); the full declaration minus its proof
proof
string… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Lean4-EquationalTheories.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.miniF2F-lean4minif2f-lean4-normalizedlean4-stat-learning-theory-novel
A Large-Scale Lean 4 Dataset on Statistical Learning Theory
We present a high-quality, human-verified, large-scale Lean 4 dataset, extracted from our formalization of Statistical Learning Theory (SLT). We present the first comprehensive Lean 4 formalization of SLT grounded in empirical process theory. Our end-to-end formal infrastructure implement the missing contents in latest Lean 4 Mathlib library, including a complete development of Gaussian Lipschitz concentration… See the full description on the dataset page: https://huggingface.co/datasets/yuanhezhang/lean4-stat-learning-theory-novel.