Skip to content

zhangir-azerbayev/mm-extract

Repository files navigation

mm-extract

Extracting human readable pre-training data from set.mm

Install metamath in the metamath-0.198 directory.

proofs.txt is generated by running echo -e "set scroll continuous\nset width 999999\nsh p */lemmon" | ./metamath ./set.mm > proofs.txt in the metamath directory. After creating it, move it from metamath-0.198 to the top level directory. Then run make_data.py.

About

Extracting human readable pre-training data from set.mm

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages