task_categories:translation size_categories:n<1K format:json modality:text library:datasets library:pandas library:mlcroissant library:polars region:us
---
task_categories:
- translation
size_categories:
- n<1K
---
# Number Theory Autoformalization Dataset

## Dataset Summary

This dataset consists of number theory problems, with informal (natural language) statements and the corresponding formal statements written in **Lean 4**. It is designed for autoformalization tasks in the domain of number theory. The dataset is made of problems from widely used mathematical benchmarks such as the Mini F2F and Putnam Bench.
  
## Dataset Structure

- **Mini F2F Subset (136 problems):** 
  - 120 problems sourced from the MATH dataset.
  - 16 custom problems created specifically for this dataset.
  - Focused on number theory problems.

- **Putnam Bench Subset (98 problems):**
  - Consists solely of number theory problems from the Putnam Bench.

The final dataset includes 234 number theory problems with a balanced test/validation split (50/50).

### Data Fields

1. **name**: A unique identifier for the problem.
2. **formal_statement**: The formal statement of the mathematical problem written in **Lean 4**.
3. **informal_statement**: The informal, natural language description of the problem, usually expressed in **LaTeX**.
4. **tags**: A list of tags related to the problem, which typically includes mathematical areas or subfields (e.g., "number theory", "algebra").
5. **header**: Contextual metadata necessary for **type-checking** the formal statements. The `header` contains information such as packages to import or additional definitions required for the formalization to be complete. Without the `header`, the formal statement may not "type-check" correctly.
6. **split**: Indicates whether the problem belongs to the `test` or `valid` set.

### Dataset Splits

| Split   | Number of Problems |
|---------|--------------------|
| Test    | 117                |
| Valid   | 117                |
| **Total** | **234**          |

## Data Example

Here’s an example of a problem from the dataset:

```json
{
  "name": "putnam_1991_b4",
  "formal_statement": "theorem putnam_1991_b4\n(p : ℕ)\n(podd : Odd p)\n(pprime : Prime p)\n: (∑ j : Fin (p + 1), (p.choose j) * ((p + j).choose j)) ≡ (2 ^ p + 1) [MOD (p ^ 2)] :=\nsorry",
  "informal_statement": "Suppose $p$ is an odd prime. Prove that $\\sum_{j=0}^p \\binom{p}{j}\\binom{p+j}{j} \\equiv 2^p+1 \\pmod{p^2}$.",
  "tags": "['number_theory', 'algebra']",
  "header": "",
  "split": "test"
}
```

## Usage

The dataset can be used directly in your code as follows:

### Loading the Dataset

You can load the dataset using the `datasets` library from Hugging Face:

```python
from datasets import load_dataset

# Load the entire dataset
dataset = load_dataset('agatha-duzan/number_theory_af')

# Load a specific split (test or validation)
test_set = dataset['test']
valid_set = dataset['valid']
```