datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
minif2f-lean4Fixing the errors in some formal statements and informal proofs of minif2f-lean4.
lean4-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.PutnamBench-lean4
PutnamBench — Lean 4 (672 problems)
Lean 4 formalizations from PutnamBench,
a benchmark of problems from the William Lowell Putnam Mathematical Competition (1962-2023).
Converted from the official GitHub repository for convenient HuggingFace datasets access.
Citation
@article{tsoukalas2024putnambench,
title={PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition},
author={George Tsoukalas and Jasper Lee and John Jennings and Jimmy Xin… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/PutnamBench-lean4.lean4-stat-learning-theory-corpus
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-corpus.proofnet-lean4less-proofnet-lean4-top1Mlean4
💎 Atomic-Lean4-Mathlib: Granular Proofs for Complex Analysis
🚀 Overview
Atomic-Lean4-Mathlib est un dataset de haute fidélité conçu pour le Process Supervision des LLMs de raisonnement (type o1, DeepSeek-R1).
Contrairement aux preuves standard de la Mathlib qui utilisent des tactiques opaques (simp, ring), ce dataset fournit des preuves décomposées à l'atome. Chaque étape logique est explicitée via des blocs calc et des réécritures (rw), permettant aux modèles… See the full description on the dataset page: https://huggingface.co/datasets/7rouz/lean4.lean4-sft-datasetleandojo-lean4-formal-informal-strings-splitLean4-Changelog-QA
Lean 4 Changelog Q&A Dataset
Dataset Description
The Lean 4 Changelog Q&A Dataset is derived from the Lean4-Changelog. Each Lean 4 changelog entry (including version, section, pull request number, and description) is converted into a single Q&A pair. This allows for straightforward question-answering tasks reflecting the evolution of Lean 4 features, bug fixes, and language decisions over time.
Dataset Structure
Each record contains the following fields:… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Lean4-Changelog-QA.less-proofnet-lean4-rankedhacking-lean4