search

InternLM / InternLM-Math

State-of-the-art bilingual open-sourced Math reasoning LLMs.
Apache License 2.0
429 stars 25 forks source link

how to get complete proofs from the LEAN-GitHub dataset #36

Closed LuoKaiGSW closed 3 months ago

LuoKaiGSW commented 3 months ago

Thank you for open-sourcing the LEAN-GitHub paper and dataset. I have a question: if I need to extract all the theorems and their complete proofs from the LEAN-GitHub dataset, is there a way to do that?

objecti0n commented 3 months ago

We provide start and end place for each theorem. You should check url@commit@file_path@start&end.

LuoKaiGSW commented 3 months ago

We provide start and end place for each theorem. You should check url@commit@file_path@start&end.

I got it. Thank you! @objecti0n