datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
mathlib-tactics
Mathlib Tactics
This dataset contains tactic invocations with associated goal states from proofs in Mathlib, the mathematical library for the Lean 4 theorem prover, extracted with lean_scout.
Extracted from the Mathlib commit with the following hash.
5ed2965256430c3649e86755f9576b54eca72435
The dataset follows this schema:
fields:
- type:
datatype: string
nullable: true
name: module
- type:
datatype: struct
children:
- type:
datatype: nat… See the full description on the dataset page: https://huggingface.co/datasets/mathlib-initiative/mathlib-tactics.mathlib-const-dep
Mathlib Constant Dependencies
This dataset contains direct constant dependency information for declarations in Mathlib, the mathematical library for the Lean 4 theorem prover, extracted with lean_scout.
Extracted from the Mathlib commit with the following hash.
0df444a360eaa60ab8c11dca51a86af692955474
The dataset follows this schema:
fields:
- type:
datatype: string
nullable: false
name: name
- type:
datatype: string
nullable: true
name: module
- type:
item:… See the full description on the dataset page: https://huggingface.co/datasets/mathlib-initiative/mathlib-const-dep.mathlib-types
Mathlib Types
This dataset contains information about types defined in Mathlib, the mathematical library for the Lean 4 theorem prover, extracted with lean_scout.
Extracted from the Mathlib commit with the following hash.
0df444a360eaa60ab8c11dca51a86af692955474
The dataset follows this schema:
fields:
- type:
datatype: string
nullable: false
name: name
- type:
datatype: string
nullable: true
name: module
- type:
datatype: string
nullable: false
name:… See the full description on the dataset page: https://huggingface.co/datasets/mathlib-initiative/mathlib-types.lean-dojo-mathlib4
Dataset Card for "lean-dojo-mathlib4"
More Information needed
mathlib_const_deps
Mathlib Const Deps
This dataset was generated with lean_scout
from the GitHub repository adamtopaz/mathlib_const_deps at commit ded17d387875019ca8ee4eca1307a07e814fe565.
Source
Source repository: adamtopaz/mathlib_const_deps
Source commit: ded17d387875019ca8ee4eca1307a07e814fe565
Hugging Face dataset repo: adamtopaz/mathlib_const_deps
Dataset URL: https://huggingface.co/datasets/adamtopaz/mathlib_const_deps
Generated at (UTC): 2026-03-27T20:57:40.590929Z
Mathlib commit… See the full description on the dataset page: https://huggingface.co/datasets/adamtopaz/mathlib_const_deps.Lean4-Mathlib
Lean4-Mathlib
Structured dataset of mathematical formalizations from the Mathlib4 library for Lean 4.
Source
Repository: https://github.com/leanprover-community/mathlib4
Commit: b9f14353520df73472ae3825fb53f86559a01319
Files: 8170
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
Verbatim… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Lean4-Mathlib.Mathlib-Normalized-Sexpr
Mathlib Normalized S-Expressions
Lean 4 proof states from Mathlib, paired with the tactic applied at each
step, in three representations extracted directly from the Lean kernel:
Source-faithful S-expressions of the goal and every hypothesis, as
Lean elaborated them.
Normalized S-expressions of the same state, with stable local-context
indices suitable for model input.
Annotated tactic syntax -- the original tactic's syntax tree with
identifier leaves resolved to the constants… See the full description on the dataset page: https://huggingface.co/datasets/jajostrains/Mathlib-Normalized-Sexpr.validation-mathlib-mathcompmathlib4-state-changetest_extract_mathlib_v2Lean3-Mathlib
Lean3-Mathlib
Declarations from mathlib3, the Lean 3 mathematical library (archived).
Source
Repository: https://github.com/leanprover-community/mathlib
Commit: 65a1391a0106c9204fe45bc73a039f056558cb83
Files: 3220
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
Verbatim proof/body, empty… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Lean3-Mathlib.mathlib_extracted
ABOUT
This is the result of running the LeanDojo extractor on Mathlib 4.18. It was extracted by Charlie Meyer, and has been published here so I can desecrate his work without bothering him.
Purpose
You could use this to fine tune language models to output in a certain format for automated theorem proving.
test_extract_mathlib_notypemathlib4_tactic_statesmathlib-informal-splitsubproofs-mathlib-v4.30.0mathlib_RL_v3mathlib-traced-tacticsrollout-premises-mathlib-v4.30.0mathlib4_summary_tactic_statespremises-mathlib-v4.30.0mathlib4test_extract_mathlib_v2_wholetrain-mathlib-mathcompcanonical-drafter-extract-mathlib
Canonical Drafter — extract data (raw)
Ground-truth drafter/premise data lifted from existing Mathlib proofs by
Training/ExtractData.lean. This is the raw pool (429303 draft rows,
664445 premise rows from: Mathlib). Every row is a real have / closed
subgoal taken from a checked proof, so there are no success/used flags to filter
on. Columns follow the uniform schema shared with the rollout dataset, so the two
pools concatenate cleanly.
config drafts
One row per… See the full description on the dataset page: https://huggingface.co/datasets/awhecmu/canonical-drafter-extract-mathlib.subproofs-mathlib-v4.29.0consts-mathlib-v4.30.0premises-mathlib-v4.31.0mathlibmathlib-gmib-topology