datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
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.leanstral-mathlib-calibration-corpora
Leanstral Mathlib calibration corpora
The sample data comes from the pinned Apache-2.0-licensed
Mathlib source tree. This
repository holds the data and curated methods documentation—but not the
separately developed builder package.
This dataset contains the calibration corpora used to pick a static FP8
activation profile for an MXFP4 W4A8 conversion of Leanstral 1.5 119B-A6B. It
publishes every candidate corpus, their manifests, the shared
iterative-development pack, and the… See the full description on the dataset page: https://huggingface.co/datasets/robbiemu/leanstral-mathlib-calibration-corpora.Lean3-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.