datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
theorem-matching
TheoremGraph Matching
Formal–informal theorem matches from the TheoremGraph paper. 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: https://huggingface.co/datasets/uw-math-ai/theorem-matching.ProofWiki-TheoremsSet of theorems scraped from Proofwiki.org.
28k Theorem and Proof pairs.