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

Dataset Card

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.