ChristianZ97/PutnamBench-lean4

---
license: apache-2.0
task_categories:
- text-generation
language:
- en
tags:
- lean4
- theorem-proving
- mathematics
- putnam
- formal-verification
size_categories:
- n<1K
---

# PutnamBench — Lean 4 (672 problems)

Lean 4 formalizations from [PutnamBench](https://github.com/trishullab/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

```bibtex
@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
and Michelle Ding and Michael Jennings and Amitayush Thakur
and Swarat Chaudhuri},
journal={arXiv preprint arXiv:2407.11214},
year={2024}
}
```

## Schema

| Field | Type | Description |
|-------|------|-------------|
| `problem_name` | `str` | Identifier, e.g. `putnam_1962_a1` |
| `formal_statement` | `str` | Full Lean 4 theorem (+ abbrevs), ending in `:= sorry` |
| `informal_statement` | `str` | English problem statement |
| `informal_solution` | `str` | Solution sketch or `"None."` |
| `tags` | `list[str]` | Categories: algebra, analysis, geometry, etc. |
| `split` | `str` | Always `"test"` |

## Usage

```python
from datasets import load_dataset

ds = load_dataset("ChristianZ97/PutnamBench-lean4")
print(len(ds["test"])) # 672
print(ds["test"][0]["problem_name"])
```

## Source

Official repo: <https://github.com/trishullab/PutnamBench>
License: Apache-2.0 (Lean 4 and Isabelle portions)