TREAT Theorem Recognition: dataset for "TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations"

TREAT (Theorem Recognition under Equivalence-preserving mAthematical Transformation): transformed theorem statements with theorem identity metadata and validation fields, theorem-level catalogs and a canonical formula pool, a fixed 960-item evaluation panel, the frozen 2,456-page Wikipedia source snapshot, schemas, checksums and reproducibility materials.

Dataset accompanying the paper TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations, 28th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2026) (https://synasc.ro/2026/).

Paper abstract. AI systems increasingly operate between flexible input representations and formal objects used by downstream tools. A key challenge is recognizing when an unfamiliar formulation denotes a known formal object. We study this challenge through theorem recognition: given an equivalence-preserving transformation of a theorem condition, a model must recover the theorem identity associated with the standard statement. We introduce TREAT, a benchmark designed to isolate this representation-dependent access problem. Rather than paraphrasing theorem text, TREAT changes the mathematical form of theorem conditions themselves, expressing known results through residual equations, witness statements, optimization identities, set relations, operator forms, and proof-intermediate characterizations. Starting from scraped theorem pages, we filter for entries with usable mathematical expression forms, extract canonical theorem conditions, and generate transformed variants with recorded assumptions and inverse mappings. The final corpus contains 737 theorem identities and 29,900 transformed rows. On a test panel, the best model retrieves the correct theorem identity in only 60.73% of cases. Other systems reveal different failure modes, including abstention, wrong-theorem commitments, and malformed structured outputs. These results suggest that theorem knowledge can be fragile under equivalent changes in representation. TREAT therefore provides a controlled testbed for evaluating representation-robust access to formal knowledge, with broader relevance to domains that require stable target objects, explicit equivalence relations, validation procedures, and auditable scoring.

Known limitations.

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

License: 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).