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.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.