Mathematical Reasoning · SAIRfoundation
equational-theories-selected-problems
Curated mathematical implication problems for benchmarking automated theorem proving and language model reasoning.
What equational-theories-selected-problems is
equational-theories-selected-problems is a curated collection of mathematical logic problems created by the SAIRfoundation for the Mathematics Distillation Challenge: Equational Theories. The challenge evaluates the capabilities of automated theorem proving systems and large language models on equational reasoning tasks over algebraic magmas.
Because evaluating models on the full implication table is computationally prohibitive, this repository extracts standardised, manageable subsets across varying difficulty tiers, ranging from programmatically sampled instances to challenging problems co-curated by human mathematicians and artificial intelligence.
The dataset spans both training subsets and evaluation benchmarks across Stage 1 and Stage 2 of the competition. It includes verified implication tasks alongside open research problems derived from order-5 Austin laws that remain undecided by existing automated reasoning tools.
How it was made
Problems are formulated as ordered pairs of equations, testing whether Equation 1 implies Equation 2 over all magmas. Problems are derived from the 4,694 laws of the Equational Theories Project for order-4 and below, or from order-5 equation lists. The subsets are sampled using programmatic selection, human curation, and collaborative human-AI methods to assemble specific difficulty profiles.
Each record contains problem identifiers, 1-based equation references, the equation strings, the designated difficulty tier, and a boolean answer indicating whether the implication holds. Certain evaluation sets temporarily withhold answers, whilst open research subsets set the answer field to null by construction because the mathematical implications remain unresolved by automated provers such as Vampire and Mace4.
Key facts
- Problem category
- Mathematical reasoning and equational theory implications
- Underlying law count
- 4,694 laws (yielding 22,028,942 possible ordered implications)
- Formats
- JSON Lines (.jsonl), JSON metadata (.json)
- Modality
- Tabular and text
- Primary splits
- All subsets exposed via the train split in datasets
What you can use it for
- Automated Theorem Prover Evaluation
- Benchmarking automated deduction tools and provers on equational logic problems across stratified difficulty levels.
- Language Model Mathematical Reasoning
- Assessing whether large language models can determine whether one algebraic equation universally implies another across all magmas.
- Open Problem Exploration
- Investigating undecided order-5 Austin law implication problems using custom heuristics, search strategies, or formal verification.
Explore the data
No licence declared
The authors have not published a licence, which means no permission to redistribute the data has been granted to anyone. The rows are not served here; read them on the original dataset page.How the columns are distributed
Over 200 rows of evaluation_extra_hard/train
answer
bool- False50%
- True50%
difficulty
string_label- extra_hard100%
eq1_id
int- min
- 24
- median
- 336
- mean
- 727.38
- max
- 3,356
eq2_id
int- min
- 8
- median
- 3,514
- mean
- 3032.42
- max
- 4,689
equation1
string_label- x = (y * x) * (x * (z * w))24%
- x = (y * x) * (x * z)20%
- x * y = y * (y * y)18%
equation2
string_text- min
- 15
- median
- 25
- mean
- 25.19
- max
- 27
id
string_text- min
- 26
- median
- 26
- mean
- 26
- max
- 26
index
int- min
- 1
- median
- 100.50
- mean
- 100.50
- max
- 200
Strengths and limits
Good at
- Provides balanced, verified subsets with equal or controlled distributions of true and false implications.
- Categorises problems across multiple clear difficulty levels, including normal, hard, extra hard, and order-5.
- Includes dedicated open research subsets containing implications unresolved by automated tooling like Vampire and Mace4.
Watch out for
- Research subsets (such as research_order5_hard and stage2_evaluation_research) lack ground-truth answers.
- The stage2_evaluation_main subset withholds ground-truth answers during the competition period.
Questions
Can I look inside equational-theories-selected-problems without downloading it?
Not here: it declares no licence, so no permission to redistribute its rows has been granted. Its description and statistics are still shown.
What licence is equational-theories-selected-problems under?
Its authors have not declared a licence, which means no permission to reuse or redistribute it has been granted.
What mathematical domain do these equations belong to?
The problems test implications between equational laws over all magmas, which are basic algebraic structures consisting of a set equipped with a single binary operation.
Why are some answer fields set to null?
Answers are set to null either because the problems represent open research questions undecided by current automated tooling, or because ground-truth labels are temporarily withheld during active competition evaluation stages.
What is the difference between the hard subsets?
The hard subset contains 200 human-AI curated problems, hard1 is a deduplicated version containing 69 unique problems, hard2 provides a balanced set of 200 problems (100 true, 100 false), and hard3 expands the curation to 400 problems.
Written from equational-theories-selected-problems's own dataset card. Statements citing a figure that does not appear there are removed before publication. Licence and running details come from our registry.