CoolFace
Datasetpublic

kamushekp/Metamath2Py

Links Github with source code: https://github.com/kamushekp/metamath2py Paper: https://github.com/kamushekp/metamath2py/blob/main/out/main.pdf Dataset Structure The Metamath2Py Dataset consists of the following components: 1. JSONL File on Hugging Face The dataset is provided as a JSONL file, where each line is a JSON object with the following fields: original_name: The original name of the statement in the Metamath system. name: The statement name… See the full description on the dataset page: https://huggingface.co/datasets/kamushekp/Metamath2Py.

sourceHugging Facemitupdated 1y agoView on Hugging Face
0likes62downloads
Dataset Card

Links

Github with source code: https://github.com/kamushekp/metamath2py

Paper: https://github.com/kamushekp/metamath2py/blob/main/out/main.pdf

Dataset Structure

The Metamath2Py Dataset consists of the following components:

1. JSONL File on Hugging Face

The dataset is provided as a JSONL file, where each line is a JSON object with the following fields:

  • —original_name: The original name of the statement in the Metamath system.
  • —name: The statement name in our dataset (modified to be compatible with Python naming conventions, see the paper for details).
  • —floatings: The translation of floating arguments from Metamath into Python.
  • —essentials: The translation of essential hypotheses from Metamath into Python.
  • —class: The translation of the statement itself from Metamath into Python.
  • —executable_class: A combined structure including floatings, essentials, and the corresponding class.
  • —executable_proof: The translation of the proof from Metamath into Python.
  • —comment: A comment associated with the statement, usually authored by the original theorem contributors (extracted from set.mm).
  • —lemmon_notation: The proof of statement in Lemmon notation, generated by metamath.exe with the /lemmon/renumber modifiers (see the Metamath book for details). Note: lemmon_notation available not for all statements, for example, for ax-mp is not $p (provable)

2. metamath2py_executables.7z Archive

This archive contains two directories:

  • —proofs/: Valid Python files representing the translated proofs.
  • —classes/: Valid Python files representing the translated statements.

3. pythonic_names_map.csv

This file stores the mapping between original Metamath statement names and their randomly generated Python-compatible names:

\<Metamath statement name\> \<Python-compatible statement name\>

4. class_variables.csv

This file stores the mapping between Metamath operator tokens and human-readable Python-compatible operation names:

\<Metamath operator token\> \<Python-compatible operator name\>

5. step_completion_v1.jsonl

This file stores evaluation for the paper. It contains LLM proof step predictions for both lemmon notation and metamath2py notation. Also, it contains scores got using LLM-as-a-judge paradigm. For more info about usage, see https://github.com/kamushekp/metamath2py/blob/main/step_completion.ipynb