Datasetpublic

harrywsanders/mathlib_extracted

ABOUT This is the result of running the LeanDojo extractor on Mathlib 4.18. It was extracted by Charlie Meyer, and has been published here so I can desecrate his work without bothering him. Purpose You could use this to fine tune language models to output in a certain format for automated theorem proving.

sourceHugging Faceupdated 1y agoView on Hugging Face

0likes24downloads

root

dirdata/

file.gitattributes2 KBdownload

filedata-00000-of-00001.arrow346.4 MBdownload

filedataset_info.json2 KBdownload

fileREADME.md1 KBdownload

filestate.json355 Bdownload

harrywsanders/mathlib_extracted · main · files are served by the source, never re-hosted here