About a year and a half ago I dove into the Metamath system with the goal of creation of LLM-based automatical theorem proover. I had trouble with the fact that Metamath seemed to be under-represented in the training sets of Chat-GPT and others, and so its syntax and proof semantics were hard for the models to understand. I solved this by rewriting mmverify.py to map Metamath’s floating and essential hypotheses, assertions, and proof steps to executable Python classes. It seemed reasonable to me to share these intermediate results and publish a short article, dataset and source code.
github repository: https://github.com/kamushekp/metamath2py/tree/main in particular, paper: https://github.com/kamushekp/metamath2py/blob/main/out/main.pdf hugginface dataset: https://huggingface.co/datasets/kamushekp/Metamath2Py I welcome any questions, feedback, or critique on the dataset, code, or paper. P.S. I’m also considering submitting this paper to arXiv, but as a first‑time submitter I need an endorsement. If anyone here can endorse me, I’d be grateful. https://arxiv.org/auth/endorse?x=NA8HI3 (Endorsement Code: NA8HI3) Best regards, Pavel -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/1f1d10d3-5113-4d2f-93cd-08b2a5a0d6c3n%40googlegroups.com.
