license:mit size_categories:10M<n<100M format:json modality:text library:datasets library:pandas library:mlcroissant library:polars region:us
---
license: mit
---

This dataset was generated using (a [fork](https://github.com/adamtopaz/equational_theories) of) T. Tao's [equational theories](https://github.com/teorth/equational_theories) project.

The file `implications.jsonl` was generated using the command `lake exe extract_implications --jsonl --closure > implications.jsonl`.
The file `tokenized_equations.jsonl` was generated using the command `lake exe tokenized_data equations > tokenized_equations.jsonl`.
The file `random_tokenized_equations.jsonl` was generated using the command lake exe tokenized_data `lake exe tokenized_data generate xyzwuvrst 10000000 1 10 > random_tokenized_equations.jsonl`.

From there, the set of equations in `implications.jsonl` was collected, shuffled, and split into two subsets of (essentially) equal size, say `A` and `B`.
The file `train_impl.json` contains only those implications whose `lhs` and `rhs` equations are *both* contained in `A`.

Similarly, the collection of implications whose `lhs` and `rhs` are both contained in `B` was computed, call it `S`. 
The set `S` was shuffled, and also split into two subsets of (essentially) equal size, say `U` and `V`.
The file `val_impl.json` contains those implications appearing in `U`, and the file `test_impl.json` contains those implications appearing in `V`.

The magma expressions appearing in the equations in `tokenized_equations.jsonl` and `random_tokenized_equations.jsonl` are tokenized using *prefix* notation.
For example, the magma expression `(x * y) * z` is tokenized as `["mul", "mul", "x", "y", "z"]` while `x * (y * z)` is tokenized as `["mul", "x", "mul", "y", "z"]`.