---
license: cc-by-sa-4.0
language:
- en
pretty_name: TREAT Dataset Release
size_categories:
- 10K<n<100K
task_categories:
- text-classification
tags:
- mathematics
- theorem-recognition
- theorem-variants
- canonicalization
- robustness
configs:
- config_name: theorem_variants
  data_files:
  - split: train
    path: benchmark/theorem_variants.csv
  default: true
- config_name: shared_known_intersection_all4_960
  data_files:
  - split: train
    path: evaluation_panels/shared_known_intersection_all4_960.csv
- config_name: raw_theorem_pages
  data_files:
  - split: train
    path: raw/raw_theorem_pages.jsonl
- config_name: canonical_formula_pool_benchmark
  data_files:
  - split: train
    path: catalog/canonical_formula_pool_benchmark.csv
- config_name: benchmark_catalog
  data_files:
  - split: train
    path: catalog/benchmark_catalog.csv
- config_name: model_provenance
  data_files:
  - split: train
    path: reproducibility/model_provenance.csv
---


# TREAT Dataset Release

TREAT stands for **Theorem Recognition under Equivalence-preserving mAthematical Transformation**. The dataset evaluates whether a model can recover the underlying named theorem from mathematically equivalent but unfamiliar formula-level representations.

This directory contains a public-facing release of the theorem-variant dataset and associated supporting artifacts. It is organized to separate the raw scraped source material, the final benchmark, theorem-level catalogs, a fixed evaluation panel, and machine-readable metadata required for verification and reuse.

## Directory Structure

```text
TREAT/
  README.md
  raw/
    raw_theorem_pages.jsonl
  benchmark/
    theorem_variants.csv
  catalog/
    benchmark_catalog.csv
    canonical_formula_pool_benchmark.csv
  evaluation_panels/
    shared_known_intersection_all4_960.csv
    shared_known_intersection_all4_960_summary.json
  reproducibility/
    README.md
    source_snapshot.md
    model_provenance.csv
    recognition_prompt.txt
    familiarity_prompt.txt
    paired_significance.py
  metadata/
    benchmark_catalog_schema.json
    benchmark_schema.json
    canonical_formula_pool_benchmark_schema.json
    checksums.sha256
    dataset_summary.json
    raw_schema.json
    release_manifest.json
    shared_panel_schema.json
```

## Release Components

### 1. Raw Source Collection

**File:** `raw/raw_theorem_pages.jsonl`

This file contains the raw scraped theorem/page collection that served as the initial intake pool for subsequent curation and benchmark construction.

- Format: JSON Lines
- Records: 2,456
- Role: upstream source archive
- Frozen: March 27, 2026
- SHA-256: `6b002898d2487c080ec7f274891eb05d3d6bad601960535a80fc803cb69c4206`

Typical record fields include:

- `title`
- `url`
- `category_path`
- `extract`
- `fullurl`
- `categories`

This is the exact preserved source text used by the project, not a reconstruction from current Wikipedia pages. It contains a mixture of directly useful theorem pages and pages later filtered, normalized, or excluded. Page revision IDs were not retained; see [`reproducibility/source_snapshot.md`](reproducibility/source_snapshot.md) for the precise reproducibility boundary.

### 2. Final Benchmark

**File:** `benchmark/theorem_variants.csv`

This is the principal benchmark release file. It contains the final collection of transformed theorem statements together with canonical theorem metadata and validation-related fields.

- Format: CSV
- Rows: 29,900
- Unique theorem identities: 737

This file is intended for experiments in:

- theorem recognition under transformation
- canonicalization and reverse mapping
- route reconstruction
- robustness to non-canonical mathematical surface forms

High-level family counts in the current release are:

- `Analysis`: 13,440
- `Probability / Information Theory`: 5,800
- `Number Theory`: 4,320
- `Algebra / Linear Algebra`: 4,100
- `Combinatorics / Graph Theory`: 2,240

Difficulty distribution:

- `easy`: 4,235
- `medium`: 4,001
- `hard`: 11,680
- `very_hard`: 9,984

### 3. Theorem-Level Catalogs

#### `catalog/benchmark_catalog.csv`

This file provides the theorem-level inventory underlying the final benchmark.

- Format: CSV
- Rows: 737
- Granularity: one row per canonical theorem identity represented in the benchmark

It is the recommended entry point for readers who require a compact overview of the canonical theorem coverage without the full variant expansion.

Representative fields include:

- `canonical_name`
- `field`
- `subfield`
- `selected_family`
- `theorem_shape`
- `expression_type`
- `formula_seed`
- `short_statement`

#### `catalog/canonical_formula_pool_benchmark.csv`

This file contains a benchmark-relevant pool of canonical formulas or defining conditions for theorem-level entries.

- Format: CSV
- Rows: 1,034

It is broader than the strict 737-theorem benchmark catalog because it retains additional formula-backed entries assembled during curation. It is the most useful file for theorem-level inspection when canonical mathematical forms are required.

### 4. Fixed Evaluation Panel

#### `evaluation_panels/shared_known_intersection_all4_960.csv`

This file contains the fixed 960-item shared evaluation panel used for same-item comparison across multiple models.

- Format: CSV
- Rows: 960

This panel is included because it is substantially easier to inspect and share than the full benchmark while still preserving benchmark-style metadata and transformed statements. It is appropriate for:

- manual review
- small-scale replication
- same-item cross-model comparison

The associated summary file is:

- `evaluation_panels/shared_known_intersection_all4_960_summary.json`

## Reproducibility and Model Use

The [`reproducibility/`](reproducibility/) directory documents the frozen source snapshot, model roles and retained identifiers, construction and evaluation provenance, prompt contracts, six exact-correctness outcome vectors, and dependency-free paired-test code.

The public artifacts support data inspection, integrity verification, panel-level rescoring, and reproduction of the reported paired tests. They do not claim bit-for-bit regeneration of commercial-model outputs; immutable provider snapshots, exact access dates, decoding settings, and complete construction traces were not retained.

## Benchmark File Structure

The final benchmark CSV contains several categories of columns:

### Theorem Identity and Taxonomy

- `theorem_name`
- `cleaned_theorem_name`
- `field`
- `subfield`
- `selected_family`
- `family`
- `theorem_shape`
- `expression_type`

### Canonical Theorem Description

- `short_statement`
- `canonical_formula_or_condition`
- `required_assumptions`

### Variant-Level Content

- `original_formula`
- `variant_formula`
- `latex_math_representation`

### Transformation and Difficulty Metadata

- `transformation_pipeline`
- `difficulty_level`

### Validation and Inverse-Mapping Metadata

- `validity_label`
- `validation_type`
- `inverse_mapping_to_original`

Exact schema definitions are provided in:

- `metadata/benchmark_schema.json`

## Metadata Files

### `metadata/release_manifest.json`

Machine-readable release manifest containing:

- file inventory
- row counts
- byte sizes
- SHA-256 hashes
- benchmark-level summary statistics

### `metadata/checksums.sha256`

Integrity file containing SHA-256 checksums for the release payload files.

### `metadata/raw_schema.json`

Schema summary for records in the raw JSONL source collection.

### `metadata/benchmark_schema.json`

Column-level schema summary for `benchmark/theorem_variants.csv`.

### `metadata/benchmark_catalog_schema.json`

Column-level schema summary for `catalog/benchmark_catalog.csv`.

### `metadata/canonical_formula_pool_benchmark_schema.json`

Column-level schema summary for `catalog/canonical_formula_pool_benchmark.csv`.

### `metadata/shared_panel_schema.json`

Column-level schema summary for `evaluation_panels/shared_known_intersection_all4_960.csv`.

### `metadata/dataset_summary.json`

Compact machine-readable summary of the release.

## Encoding

All files are distributed in UTF-8-compatible formats:

- `raw/raw_theorem_pages.jsonl`: UTF-8 JSON Lines
- `benchmark/theorem_variants.csv`: UTF-8 CSV
- supporting CSV files: UTF-8 CSV
- metadata files: UTF-8 JSON or text

If a downstream system has limited Unicode support, explicit UTF-8 import settings are recommended.

## Recommended Usage

The files in this release serve different purposes:

- use `benchmark/theorem_variants.csv` for the full transformed-theorem benchmark
- use `catalog/benchmark_catalog.csv` for theorem-level benchmark coverage
- use `catalog/canonical_formula_pool_benchmark.csv` when canonical formulas or conditions are needed
- use `evaluation_panels/shared_known_intersection_all4_960.csv` for smaller fixed-panel evaluation or manual inspection
- use `raw/raw_theorem_pages.jsonl` only when access to the original scrape-level source material is required

## License and Attribution

This release is distributed under CC BY-SA 4.0 because the source collection is derived from public Wikipedia theorem pages. Downstream users should preserve source attribution, including page titles and URLs where present in the released files.

For reuse, cite this dataset as described in `CITATION.cff`.

## Known Limitations

TREAT is a benchmark of representation-robust theorem recognition, not a fully formal proof corpus. The transformed rows include validation metadata and inverse-mapping notes, but not every row has a machine-checkable proof certificate. Users who require formally certified theorem transformations should filter by the validation columns and/or perform additional domain-specific review.

<!-- BEGIN GENERATED METADATA (_publishing/generate_metadata.py) -->

## Dataset card

| | |
|---|---|
| **Paper** | [TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations](https://synasc.ro/2026/) |
| **Venue** | 28th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2026) |
| **Authors** | Fateme Mazdarani, Carlos Toxtli |
| **License** | Creative Commons Attribution-ShareAlike 4.0 International (`cc-by-sa-4.0`) |
| **Dataset DOI** | [10.5281/zenodo.24179071](https://doi.org/10.5281/zenodo.24179071) |
| **Version** | 1.0.0 |
| **Code repository** | https://github.com/mazdarani/TREAT |
| **Maintainer** | [Human-AI Empowerment Lab, Clemson University](https://haielab.org) |

## Dataset structure

| Path | Format | Size | Records |
|---|---|---|---|
| `benchmark/theorem_variants.csv` | csv | 32.5 MB | 29,900 |
| `catalog/benchmark_catalog.csv` | csv | 246.6 KB | 737 |
| `catalog/canonical_formula_pool_benchmark.csv` | csv | 395.2 KB | 1,034 |
| `evaluation_panels/shared_known_intersection_all4_960.csv` | csv | 979.0 KB | 960 |
| `evaluation_panels/shared_known_intersection_all4_960_summary.json` | json | 4.0 KB |  |
| `metadata/benchmark_catalog_schema.json` | json | 1.1 KB |  |
| `metadata/benchmark_schema.json` | json | 2.8 KB |  |
| `metadata/canonical_formula_pool_benchmark_schema.json` | json | 1.0 KB |  |
| `metadata/checksums.sha256` | sha256 | 1.2 KB |  |
| `metadata/dataset_summary.json` | json | 1.8 KB |  |
| `metadata/raw_schema.json` | json | 633 B |  |
| `metadata/release_manifest.json` | json | 3.8 KB |  |
| `metadata/shared_panel_schema.json` | json | 2.7 KB |  |
| `raw/raw_theorem_pages.jsonl` | jsonl | 41.6 MB | 2,456 |
| `reproducibility/README.md` | md | 5.7 KB |  |
| `reproducibility/familiarity_prompt.txt` | txt | 338 B |  |
| `reproducibility/model_provenance.csv` | csv | 2.3 KB | 10 |
| `reproducibility/paired_significance.py` | py | 7.5 KB |  |
| `reproducibility/recognition_prompt.txt` | txt | 817 B |  |
| `reproducibility/source_snapshot.md` | md | 1.1 KB |  |

20 files, 75.7 MB in total (metadata files excluded). Records are rows for CSV/TSV/JSONL files and list length for JSON arrays.

## Loading the data

```python
from datasets import load_dataset

ds = load_dataset("ai4he/treat-theorem-recognition", "theorem_variants")
```

Available subsets: `theorem_variants`, `shared_known_intersection_all4_960`, `raw_theorem_pages`, `canonical_formula_pool_benchmark`, `benchmark_catalog`, `model_provenance`. All other files can be downloaded with `huggingface_hub.snapshot_download` or from the Zenodo record.

## Known limitations

- Wikipedia revision IDs were not recorded; a new crawl will not reproduce the archived source exactly.

## Personal and sensitive information

None.

## License

The data and documentation are released under the [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Derived from English Wikipedia theorem pages (CC BY-SA 4.0).

## Citation

If you use this dataset, please cite the paper:

```bibtex
@inproceedings{Mazdarani2026TREAT,
 title = {TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations},
 author = {Mazdarani, Fateme and Toxtli, Carlos},
 booktitle = {Proceedings of the 28th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2026)},
 publisher = {IEEE},
 year = {2026},
 note = {Forthcoming},
 url = {https://synasc.ro/2026/}
}
```

and the dataset:

```bibtex
@dataset{Mazdarani2026TreatTheoremRecognitionData,
  author = {Mazdarani, Fateme and Toxtli, Carlos},
  title = {{TREAT Theorem Recognition}: Dataset for ``TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations''},
  year = {2026},
  version = {1.0.0},
  publisher = {Zenodo},
  doi = {10.5281/zenodo.24179071},
  url = {https://doi.org/10.5281/zenodo.24179071}
}
```

<!-- END GENERATED METADATA -->