datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
mathlib4_dependency_graph
MATHLIB4 DEPENDENCY GRAPH
make dependency graph for mathlib4 using jixia
HOW TO
how to make your own mathlib4 graph
Clone the repository at https://github.com/fbundle/mathlib4_dependency_graph
Check out your favorite mathlib version
Use build script to build mathlib and jixia
Extract dependency graph by jixia_export.py
Get symbol file by get_symbol_file.py and get_symbol_db.py
Upload to huggingface using upload_huggingface.py
or just download the prebuilt files… See the full description on the dataset page: https://huggingface.co/datasets/khanh2023/mathlib4_dependency_graph.lean-dojo-mathlib4
Dataset Card for "lean-dojo-mathlib4"
More Information needed
mathlib4-state-changemathlib4-v4.26.0-premises
Mathlib v4.26.0 Premise Corpus (via LeanDojo-v2, fully Dockerized)
本仓库包含从 Mathlib v4.26.0(连同其全部依赖:Lean 核心库、Batteries、Aesop 等)中
提取出的全部有效 premises,以 corpus.jsonl 形式存储,可直接用于构建向量召回 / premise
selection 数据库。提取过程完全在 Docker 容器内完成,无需在本机安装 lean4 / elan / lake。
项目
值
来源仓库
leanprover-community/mathlib4
版本 / commit
v4.26.0 / 2df2f0150c275ad53cb3c90f7c98ec15a56a1a67
Lean toolchain
leanprover/lean4:v4.26.0
build_deps
true(含全部依赖)
文件数
9,765
premises 总数
284,372
corpus.jsonl… See the full description on the dataset page: https://huggingface.co/datasets/CHENSEE/mathlib4-v4.26.0-premises.mathlib4_tactic_stateselan_mathlib4_newmathlib4_summary_tactic_statesmathlib4-buildmathlib4mathlib4elan_mathlib4-92c2d0cbb4aa68ea1be62aaf7c3517f7f8e1f385mathlib4-thmsmathlib4-2-11mathlib4_v2mathlib4-ds