This repo contains the data and the scripts used for the paper.
In this repo the script main.py is provided. its purpose is to filter lean4_workbook theorems and retrieve them, called without args it returns a list of proven theorems with the associated index (referenced in the data). Called with a theorem index it will return all the details about that specific theorem.
Theorems and proofs on which LLMs are tested are in the lean4 workbook, that can by retrieved by git cloning it:
git clone https://huggingface.co/datasets/internlm/Lean-Workbook
Results of our testing are contained in data.csv and summarized in data_summary.csv. livebench.csv contains the current (12/11/2024) benchmarks results for the tested LLMs.
The following prompts have been used to test the LLMs.
translate this statement in lean4, don't prove it and provide only lean4 translation without description
<lean_workbook natural language statement>
proof this in lean4, explain the code in depth step by step and give the complete solution as code at the end
<lean_workbook lean4 statement>
is this a valid Lean4 proof?
<lean_workbook statement and proof in lean4>