uw-math-ai/theorem-search-dataset-permissive

--- license: cc-by-4.0 task_categories: - question-answering - feature-extraction - sentence-similarity language: - en tags: - math - theorems - semantic-search - information-retrieval - LaTeX - arXiv size_categories: - 1M<n<10M pretty_name: Theorem Search Dataset configs: - config_name: default data_files: - split: train path: - paper.parquet - theorem.parquet - theorem_slogan.parquet - split: test path: theorems-test.parquet --- # Theorem Search Dataset The **largest** open corpus of informal mathematical theorems: **1,239,720 theorem statements** with natural-language slogans from **197,889 papers**, designed for semantic theorem retrieval. **Paper:** [Semantic Search over 9 Million Mathematical Theorems](https://arxiv.org/abs/2602.05216) **Demo:** [huggingface.co/spaces/uw-math-ai/theorem-search](https://huggingface.co/spaces/uw-math-ai/theorem-search) ## Benchmark results On 110 test queries written by research mathematicians, our best pipeline (Qwen3-Embedding-8B on DeepSeek-V3.1 slogans) outperforms all existing tools for finding theorems in the literature: | Method | Theorem Hit@20 | Paper Hit@20 | |---|---|---| | arXiv Search | -- | 2.7% | | Google Search (`site:arxiv.org`) | -- | 37.8% | | ChatGPT 5.2 w/ Search | 19.8% | -- | | Gemini 3 Pro | 27.0% | -- | | **Ours (Qwen3 8B)** | **45.0%** | **56.8%** | ## Why this dataset? Mathematicians and AI proof assistants need to find whether a specific result already exists in the literature. Existing tools (Google Scholar, arXiv search, LLMs with web access) operate at the *paper* level, forcing users to manually scan documents for individual statements. This dataset enables **theorem-level** semantic search by pairing every theorem with a concise natural-language slogan. ## Dataset summary | | Count | |---|---| | Theorems | 1,239,720 | | Papers | 197,889 | | Slogans | 1,239,720 | | Test queries (human-written) | 110 | **Sources** (by number of theorems): arXiv (1,238,975), Open Logic Project (745). > **Note on dataset size:** The full corpus described in our paper contains over **9.2 million** theorems from approximately 690,000 arXiv papers. This dataset releases only the subset with licenses compatible with CC BY 4.0: arXiv papers under CC0, CC BY 4.0, CC BY 3.0, or CC Public Domain, plus the Open Logic Project (CC BY 4.0). Sources with ShareAlike, GFDL, or no open license are excluded. The full 9.2M-theorem corpus powers the [live demo](https://huggingface.co/spaces/uw-math-ai/theorem-search). ## Files | File | Rows | Size | Description | |---|---|---|---| | `paper.parquet` | 197,889 | 137 MB | Paper metadata (title, authors, abstract, arXiv categories, citations, etc.) | | `theorem.parquet` | 1,239,720 | 247 MB | Theorem statements in LaTeX (name, body, label, parsing method) | | `theorem_slogan.parquet` | 1,239,720 | 179 MB | Natural-language slogans generated by DeepSeek-V3.1 | | `theorems-test.parquet` | 110 | 12 KB | Human-written test queries with ground-truth theorem matches | ## Schema ### `paper.parquet` | Column | Type | Description | |---|---|---| | `paper_id` | string | Unique paper identifier (arXiv ID or source-specific tag) | | `title` | string | Paper title | | `authors` | string | List of authors | | `link` | string | URL to the paper | | `last_updated` | string | Last update date (arXiv papers) | | `summary` | string | Paper abstract | | `journal_ref` | string | Journal reference, if published | | `primary_category` | string | Primary arXiv category (e.g., `math.AG`) | | `categories` | string | All arXiv categories | | `citations` | int | Citation count (where available) | | `source` | string | Provenance: `arXiv` or `Open Logic Project` | | `license` | string | License of the source paper | ### `theorem.parquet` | Column | Type | Description | |---|---|---| | `theorem_id` | int | Unique theorem identifier | | `paper_id` | string | Foreign key to `paper.parquet` | | `name` | string | Theorem name as displayed in source (e.g., "Theorem 3.1") | | `body` | string | Full theorem statement in LaTeX | | `label` | string | LaTeX `\label{}` tag from the source | | `link` | string | Direct URL to the theorem (where available) | | `parsing_method` | string | How the theorem was extracted: `plastex`, `tex`, `regex`, or `manual` | ### `theorem_slogan.parquet` | Column | Type | Description | |---|---|---| | `slogan_id` | int | Unique slogan identifier | | `theorem_id` | int | Foreign key to `theorem.parquet` | | `model` | string | LLM used to generate the slogan (`DeepSeek-V3.1`) | | `prompt_id` | string | Prompt variant used (`body-only-v1`) | | `slogan` | string | Natural-language summary of the theorem | ### `theorems-test.parquet` | Column | Type | Description | |---|---|---| | `query` | string | Natural-language query written blind by a research mathematician | | `theorem number` | string | Ground-truth theorem identifier (e.g., "Theorem 3.1") | | `paper title` | string | Title of the paper containing the target theorem | | `link to paper on arxiv` | string | arXiv URL of the target paper | ## How theorems were extracted Theorems were parsed from LaTeX sources using three strategies, applied in fallback order: 1. **plasTeX** (956,194 theorems): LaTeX sources are converted into a structured node tree using [plasTeX](https://github.com/plastex/plastex). Theorem environments are identified and their name, number, and body extracted from node metadata. 2. **TeX logging** (296,239 theorems): A custom LaTeX package is injected that logs theorem data during compilation, capturing the theorem type, number, and body. 3. **Regex** (88,607 theorems): Regular expressions identify theorem delimiter tokens (`\begin{theorem}...\end{theorem}`, `\proclaim...\endproclaim`, etc.) and extract the body. The remaining 43 theorems were entered manually. Author-defined macros (e.g., `\R` for `\mathbb{R}`) are expanded in theorem bodies. Malformed extractions (e.g., truncated bodies shorter than 8 characters) are filtered out. ## How slogans were generated Each theorem body is passed to **DeepSeek-V3.1** with a prompt instructing the model to produce a concise, declarative English description of the theorem's main result, avoiding symbolic notation, proof details, and references to the surrounding document. Temperature is fixed at 0.2 with a maximum of 1024 output tokens. ## Test set The test set contains **110 queries** written by four research mathematicians (Giovanni Inchiostro, Dori Bejleri, Michele Pernice, Ignacio Tejeda) across 14 arXiv tags, primarily Algebraic Geometry (`math.AG`), Analysis (`math.AP`), and Geometric Measure Theory (`math.CA`, `math.MG`). ## Quick start ```python import pandas as pd # Load the dataset papers = pd.read_parquet("paper.parquet") theorems = pd.read_parquet("theorem.parquet") slogans = pd.read_parquet("theorem_slogan.parquet") test = pd.read_parquet("theorems-test.parquet") # Join theorems with their slogans df = theorems.merge(slogans, on="theorem_id") # Example: find all theorems from the Stacks Project "Algebra" chapter paper_theorems = df[df["paper_id"] == "00AO"] for _, row in paper_theorems.head(3).iterrows(): print(f"{row['name']}: {row['slogan'][:100]}...") ``` ```python # Using Hugging Face datasets from datasets import load_dataset ds = load_dataset("uw-math-ai/theorem-search-dataset") ``` ## Citation ```bibtex @article{alexander2026semantic, title = {Semantic Search over 9 Million Mathematical Theorems}, author = {Alexander, Luke and Leonen, Eric and Szeto, Sophie and Remizov, Artemii and Tejeda, Ignacio and Inchiostro, Giovanni and Ilin, Vasily}, journal= {arXiv preprint arXiv:2602.05216}, year = {2026}, doi = {10.48550/arXiv.2602.05216}, url = {https://arxiv.org/abs/2602.05216} } ``` ## Contact For questions or issues, contact [Vasily Ilin](https://vilin97.github.io/).