charliemeyer2000/ai4math-lean

---
license: apache-2.0
task_categories:
- text-generation
language:
- en
tags:
- lean4
- theorem-proving
- formal-mathematics
- verification
- math
size_categories:
- 1M<n<10M
configs:
- config_name: compfiles
data_files:
- split: train
path: data/compfiles/train-*.parquet
- config_name: deepseek_prover
data_files:
- split: train
path: data/deepseek_prover/train-*.parquet
- config_name: deepseek_proverbench
data_files:
- split: train
path: data/deepseek_proverbench/train-*.parquet
- config_name: formal_conjectures
data_files:
- split: train
path: data/formal_conjectures/train-*.parquet
- config_name: formalmath
data_files:
- split: train
path: data/formalmath/train-*.parquet
- config_name: goedel_minif2f
data_files:
- split: train
path: data/goedel_minif2f/train-*.parquet
- config_name: goedel_mobench
data_files:
- split: train
path: data/goedel_mobench/train-*.parquet
- config_name: goedel_pset
data_files:
- split: train
path: data/goedel_pset/train-*.parquet
- config_name: goedel_test
data_files:
- split: train
path: data/goedel_test/train-*.parquet
- config_name: hf_lean_workbook
data_files:
- split: train
path: data/hf_lean_workbook/train-*.parquet
- config_name: hf_minif2f_lean4
data_files:
- split: train
path: data/hf_minif2f_lean4/train-*.parquet
- config_name: hf_minif2f_v2
data_files:
- split: train
path: data/hf_minif2f_v2/train-*.parquet
- config_name: hf_tonic_minif2f
data_files:
- split: train
path: data/hf_tonic_minif2f/train-*.parquet
- config_name: lean_proofs
data_files:
- split: train
path: data/lean_proofs/train-*.parquet
- config_name: lean_workbook_full
data_files:
- split: train
path: data/lean_workbook_full/train-*.parquet
- config_name: matholympiadbench
data_files:
- split: train
path: data/matholympiadbench/train-*.parquet
- config_name: nemotron_proofs
data_files:
- split: train
path: data/nemotron_proofs/train-*.parquet
- config_name: numinamath_lean
data_files:
- split: train
path: data/numinamath_lean/train-*.parquet
- config_name: proofnet
data_files:
- split: train
path: data/proofnet/train-*.parquet
- config_name: putnam2025
data_files:
- split: train
path: data/putnam2025/train-*.parquet
- config_name: putnam_bench
data_files:
- split: train
path: data/putnam_bench/train-*.parquet
dataset_info:
features:
- name: id
dtype: string
- name: source
dtype: string
- name: formal_statement
dtype: string
- name: header
dtype: string
- name: lean4_code
dtype: string
- name: has_proof
dtype: bool
- name: proof_body
dtype: string
- name: natural_language
dtype: string
- name: lean_version
dtype: string
- name: split
dtype: string
- name: tags
sequence: string
- name: category
dtype: string
- name: verification
dtype: string
- name: v4210_is_valid
dtype: bool
- name: v4210_compiles
dtype: bool
- name: v4210_has_sorry
dtype: bool
- name: v4210_latency_s
dtype: float64
---

# ai4math-lean

21 Lean 4 formal mathematics datasets with machine-verified labels.

Every problem has been verified against lean-server v4.21.0 on UVA's HPC cluster.
Results are embedded in each row as both structured `verification` JSON and flattened convenience columns.

## Quick Start

```python
from datasets import load_dataset

# Load a single dataset
ds = load_dataset("charliemeyer2000/ai4math-lean", "deepseek_prover")

# Load a large dataset with streaming
ds = load_dataset("charliemeyer2000/ai4math-lean", "goedel_pset", streaming=True)

# Filter to valid proofs
valid = ds.filter(lambda x: x["v4210_is_valid"] == True)

# Filter to RL targets (compiles but no proof)
rl = ds.filter(lambda x: x["v4210_compiles"] and not x["has_proof"])
```

## Totals

| Metric | Count |
|--------|-------|
| Total problems | 3,394,310 |
| With proofs (SFT) | 1,273,472 |
| Valid on v4.21.0 | 352,065 |

## Datasets

| Dataset | Problems | Proofs | Valid v4.21.0 |
|---------|----------|--------|---------------|
| compfiles | 297 | 259 | 67 |
| deepseek_prover | 27,503 | 27,503 | 27,126 |
| deepseek_proverbench | 325 | 0 | 0 |
| formal_conjectures | 618 | 13 | 13 |
| formalmath | 5,560 | 5,556 | 2 |
| goedel_minif2f | 244 | 0 | 0 |
| goedel_mobench | 360 | 0 | 0 |
| goedel_pset | 1,732,594 | 263,589 | 9,755 |
| goedel_test | 8 | 0 | 0 |
| hf_lean_workbook | 29,750 | 29,750 | 29,208 |
| hf_minif2f_lean4 | 231 | 0 | 0 |
| hf_minif2f_v2 | 488 | 0 | 0 |
| hf_tonic_minif2f | 488 | 0 | 0 |
| lean_proofs | 98 | 97 | 15 |
| lean_workbook_full | 140,214 | 0 | 0 |
| matholympiadbench | 360 | 0 | 0 |
| nemotron_proofs | 1,349,950 | 915,078 | 285,867 |
| numinamath_lean | 104,155 | 31,615 | 0 |
| proofnet | 371 | 0 | 0 |
| putnam2025 | 24 | 12 | 12 |
| putnam_bench | 672 | 0 | 0 |

## Schema

Each row contains:

| Field | Type | Description |
|-------|------|-------------|
| `id` | string | Unique problem identifier |
| `source` | string | Dataset source name |
| `formal_statement` | string | Lean 4 theorem statement (no proof body) |
| `header` | string | Import/setup code |
| `lean4_code` | string | Full runnable Lean 4 code |
| `has_proof` | bool | True if contains a real proof (not sorry) |
| `proof_body` | string? | Proof tactic block (if has_proof) |
| `natural_language` | string? | NL problem statement (if available) |
| `lean_version` | string? | Original Lean toolchain version |
| `split` | string? | train/test/val split |
| `tags` | list[string] | Tags (topic, difficulty, etc.) |
| `category` | string? | Math category |
| `verification` | string (JSON) | Full verification results per Lean version |
| `v4210_is_valid` | bool? | True=valid, False=errors/sorry, None=timeout |
| `v4210_compiles` | bool | Whether the code compiled (is_valid is not None) |
| `v4210_has_sorry` | bool? | Whether sorry was detected |
| `v4210_latency_s` | float? | Verification wall time in seconds |

## Verification Details

The `verification` column contains a JSON string mapping Lean versions to results:

```json
{
"v4.21.0": {
"is_valid": false,
"has_sorry": true,
"errors": [],
"timeout_s": 600.0,
"latency_s": 34.59,
"verified_at": "2026-03-26T21:57:47Z"
}
}
```

## License

Apache 2.0