README
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.
Contributors
15 commits
Similar repos
Languages
Python
100.0%
README
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.
Similar repos
Contributors
15 commits
Languages
Python
100.0%