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.