Table · dataset · 2026
TheoremGraph Matching
Listed in Hugging Face Datasets
TheoremGraph Matching Formal–informal theorem matches from the TheoremGraph paper.
Description
Each row pairs a Lean declaration with the most similar natural-language statement from arXiv, found by cosine similarity over slogan embeddings, and labeled by an LLM judge as exact, inexact, or wrong (the first two count as a match). The file contains every candidate pair at cosine similarity 0.80 and above: 100,831 pairs.
Our primary judge, GPT-5.4, labels 47,952 of them as matches; a second… See the full description on the dataset page: huggingface.co/datasets/uw-math-ai/theorem-matching.
Links
Where it is published
- Hugging Face dataset page huggingface.co/datasets/uw-math-ai/theorem-matching ↗
landing page · from Hugging Face
Catalogue records · 1
- Hub API huggingface.co/api/datasets/uw-math-ai/theorem-matching ↗
metadata API · from Hugging Face
Topics
- Stated by source
- text · text classification · text retrieval
- From keywords
- Computer Science & AI · Mathematics & Statistics
Provenance · 1 source records, 12 field assertions
| Source | Key | Last seen | Raw |
|---|---|---|---|
| Hugging Face Datasets | uw-math-ai/theorem-matching | 15 d ago | JSON v1 |
| Field | Assertion | Extractor | Evidence |
|---|---|---|---|
| access_level | source · Hugging Face | connector:huggingface@1.0.0 | /gated |
| concepts[field].local:field:computer-science-ai | mapping · Hugging Face | connector:huggingface@1.0.0 | |
| concepts[field].local:field:mathematics-statistics | mapping · Hugging Face | vocabulary-mapper@1.0.0 | keywords['mathematics'] |
| concepts[modality].hf_modality:text | source · Hugging Face | connector:huggingface@1.0.0 | |
| concepts[task].hf_task:text-classification | source · Hugging Face | connector:huggingface@1.0.0 | /tags[task_categories:*] |
| concepts[task].hf_task:text-retrieval | source · Hugging Face | connector:huggingface@1.0.0 | /tags[task_categories:*] |
| created_date | source · Hugging Face | connector:huggingface@1.0.0 | |
| description | source · Hugging Face | connector:huggingface@1.0.0 | /description |
| license | source · Hugging Face | connector:huggingface@1.0.0 | /tags[license:*] |
| publication_date | source · Hugging Face | connector:huggingface@1.0.0 | |
| title | source · Hugging Face | connector:huggingface@1.0.0 | /id |
| updated_date | source · Hugging Face | connector:huggingface@1.0.0 |